∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X]
  (x y : Metric.Snowflaking X α hα₀ hα₁),
  dist (Metric.Snowflaking.ofSnowflaking x) (Metric.Snowflaking.ofSnowflaking y) = dist x y ^ α⁻¹