proposition: Lemma StepFSupBall_triangle : forall e d (x y z:StepF (msp_as_RSetoid X)), (StepFSupBall e x y) -> (StepFSupBall d y z) -> (StepFSupBall (e+d) x z).
proof: Proof. intros e d x y z. unfold StepFSupBall. set (be:=(@ballS X e)). set (bd:=(@ballS X d)). set (bed:=(@ballS X (e+d) )). intro H. apply StepF_imp_imp. revert H. apply StepF_imp_imp. unfold StepF_imp. pose (f:= ap (compose (@ap _ _ _) (compose (compose (compose (@compose _ _ _) imp)) be)) (compose (flip (compose (@ap _ _ _) (compose (compose imp) bd))) bed)). cut (StepFfoldProp (f ^@> x <@> y <@> z)). unfold f. evalStepF. tauto. apply StepFfoldPropForall_Map3. apply: (ball_triangle X e d). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionSetoid CoRN.metric2.StepFunctionMonad CoRN.metric2.UniformContinuity CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.metric2.Prelength CoRN.algebra.COrdFields2 CoRN.tactics.CornTac