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