∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [NormedAddTorsor V P] (a b c d : P), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d