∀ {E : Type u_1} [inst : Norm E] [inst_1 : AddGroup E] [inst_2 : PseudoMetricSpace E],
  (∀ (x : E), ‖x‖ = dist x 0) → (∀ (x y z : E), dist x y ≤ dist (x + z) (y + z)) → ∀ (x y : E), dist x y = ‖x - y‖