proposition: Lemma AffineLe : forall {R : ConstructiveReals} (a b c d x low up : CRcarrier R), a * low + b <= c * low + d -> a * up + b <= c * up + d -> low <= x <= up -> a * x + b <= c * x + d.
proof: Proof. intro R. assert (forall (a b x low up : CRcarrier R), 0 <= a * low + b -> 0 <= a * up + b -> low <= x <= up -> 0 <= a * x + b). { intros. apply (CRle_trans _ (CRmin (a*low+b) (a*up+b))). apply CRmin_glb; assumption. rewrite CRplus_comm, (CRplus_comm (a*up)), <- CRmin_plus, CRplus_comm. apply CRplus_le_compat_r. intro abs. apply CRlt_min in abs. destruct abs. clear H H0. apply CRlt_minus in c. pose proof (CRmult_pos_appart_zero a (low-x)). destruct H. apply (CRlt_le_trans _ _ _ c). unfold CRminus. rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. apply CRle_refl. + contradict c. apply (CRle_trans _ (a * (low - x))). unfold CRminus. rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. apply CRle_refl. rewrite <- (CRmult_0_r a). apply CRmult_le_compat_l. apply CRlt_asym, c1. rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r. exact (proj1 H1). + apply CRopp_gt_lt_contravar in c0. contradict c0. fold (-(a*x) <= -(a*up)). do 2 rewrite CRopp_mult_distr_l. apply CRmult_le_compat_l. rewrite <- CRopp_0. apply CRopp_ge_le_contravar, CRlt_asym, c1. exact (proj2 H1). } intros. apply (CRplus_le_reg_r (-(a*x+b))). rewrite CRplus_opp_r, CRopp_plus_distr, CRplus_assoc. rewrite (CRplus_comm d), <- CRplus_assoc, <- CRplus_assoc. rewrite CRopp_mult_distr_l, <- CRmult_plus_distr_r. rewrite CRplus_assoc. apply (H (c-a) (-b+d) x low up). 3: exact H2. rewrite (CRplus_comm (-b)), <- CRplus_assoc. apply (CRplus_le_reg_r b). rewrite CRplus_0_l, CRplus_assoc, CRplus_opp_l, CRplus_0_r. unfold CRminus. rewrite CRmult_plus_distr_r, CRplus_comm, <- CRplus_assoc. apply (CRplus_le_reg_r (a*low)). rewrite CRplus_assoc, <- CRopp_mult_distr_l, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm, (CRplus_comm d). exact H0. rewrite (CRplus_comm (-b)), <- CRplus_assoc. apply (CRplus_le_reg_r b). rewrite CRplus_0_l, CRplus_assoc, CRplus_opp_l, CRplus_0_r. unfold CRminus. rewrite CRmult_plus_distr_r, CRplus_comm, <- CRplus_assoc. apply (CRplus_le_reg_r (a*up)). rewrite CRplus_assoc, <- CRopp_mult_distr_l, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm, (CRplus_comm d). exact H1. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia