∀ {P₁ : Type u_1} {P₂ : Type u_2} [inst : MetricSpace P₁] [inst_1 : MetricSpace P₂] {a b c : P₁} {a' b' c' : P₂},
  dist a' b' ≠ 0 → dist a b / dist a' b' = dist b c / dist b' c' → dist a b = dist a b / dist a' b' * dist a' b'