proposition: Lemma StepQ_le_trans:forall x y z, (x <= y)-> (y <= z) ->(x <= z).
proof: Proof. intros x y z. unfold StepQ_le. intros H. apply StepF_imp_imp. revert H. apply StepF_imp_imp. unfold StepF_imp. pose (f:= ap (compose (@ap _ _ _) (compose (compose (compose (@compose _ _ _) imp)) QleS)) (compose (flip (compose (@ap _ _ _) (compose (compose imp) QleS))) QleS)). cut (StepFfoldProp (f ^@> x <@> y <@> z)). unfold f. evalStepF. tauto. apply StepFfoldPropForall_Map3. intros a b c Hab Hbc. clear f. simpl in *. eauto with qarith. 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