proposition: Lemma StepQabs_triangle : forall x y, StepQabs (x+y) <= StepQabs x + StepQabs y.
proof: Proof. intros x y. set (f:=(ap (compose ap (compose (compose (compose QleS QabsS)) QplusS)) (compose (flip (@compose _ _ _) QabsS) (compose QplusS QabsS)))). cut (StepFfoldProp (f ^@> x <@> y)). unfold f. evalStepF. tauto. apply StepFfoldPropForall_Map2. intros a b. apply: Qabs_triangle. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.metric2.Qmetric Coq.QArith.QArith CoRN.metric2.StepFunctionSetoid Coq.QArith.Qabs Coq.Bool.Bool CoRN.tactics.CornTac CoRN.logic.CornBasics CoRN.algebra.RSetoid