proposition: Lemma Qmax_affineCombo : forall x a b o, a < b -> (Qmax (Qmax (x - a) (affineCombo o a b - x)) (Qmax (x - affineCombo o a b) (b - x)) == Qmax (x - a) (b - x))%Q.
proof: Proof. intros x a b o H. rewrite <- Qmax_assoc. rewrite -> (Qmax_assoc (affineCombo o a b - x)). rewrite -> (Qmax_comm (affineCombo o a b - x)). rewrite <- (Qmax_assoc (x - affineCombo o a b)). rewrite -> Qmax_assoc. apply Qmax_compat. rewrite <- Qle_max_l. apply: plus_resp_leEq_lft;simpl; auto with *. rewrite <- Qle_max_r. apply: plus_resp_leEq;simpl;auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.metric2.IntegrableFunction CoRN.model.metric2.BoundedFunction CoRN.model.metric2.CRmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.ftc.Integral CoRN.model.structures.StepQsec CoRN.model.structures.OpenUnit CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetric CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.model.metric2.Qmetric CoRN.reals.fast.ContinuousCorrect CoRN.ftc.IntegrationRules CoRN.ftc.MoreIntegrals CoRN.tactics.CornTac CoRN.model.metric2.LinfDistMonad