proposition: Lemma Integral_resp_le :forall x y, x <= y -> (IntegralQ x <= IntegralQ y)%Q.
proof: Proof. intros x y H. rewrite -> Qle_minus_iff. rewrite -> Integral_opp, Integral_plus. apply Integral_resp_nonneg. revert H. apply StepF_imp_imp. unfold StepF_imp. rewriteStepF. set (g:= QleS 0). pose (f:=(ap (compose (@ap _ _ _) (compose (compose imp) QleS)) (compose (compose g) (compose (flip QplusS) QoppS)))). cut (StepFfoldProp (f ^@> x <@> y)). unfold f. evalStepF. tauto. apply StepFfoldPropForall_Map2. intros a b. change (a <= b -> 0 <= b + (- a))%Q. rewrite -> Qle_minus_iff. tauto. 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