proposition: Lemma L1ball_triangle : forall e d x y z, (L1Ball e x y) -> (L1Ball d y z) -> (L1Ball (e+d) x z).
proof: Proof. intros e d x y z. unfold L1Ball, L1Distance. unfold L1Norm. setoid_replace (x-z) with ((x-y)+(y-z)); [| ring]. intros He Hd. autorewrite with QposElim. apply Qle_trans with (IntegralQ (StepQabs (x-y) + StepQabs (y-z)))%Q. apply Integral_resp_le. apply StepQabs_triangle. rewrite <- Integral_plus. apply: plus_resp_leEq_both; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac