∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [hp : Fact (1 ≤ p)] (x y z : ↥(MeasureTheory.Lp E p μ)), dist x z ≤ dist x y + dist y z