proposition: Lemma StepApproxLe : forall {R : ConstructiveReals} (c s1 t1 s2 t2 : CRcarrier R) (ltst1 : s1 < t1) (ltst2 : s2 < t2), s1 <= s2 -> t1 <= t2 -> CRinv R (t2 - s2) (inr (CRlt_minus s2 t2 ltst2)) * (CRmin c t2 + - CRmin c s2) <= CRinv R (t1 - s1) (inr (CRlt_minus s1 t1 ltst1)) * (CRmin c t1 + - CRmin c s1).
proof: Proof. intros. destruct (CRltLinear R) as [_ s]. destruct (s s2 c t2 ltst2). - rewrite (CRmin_right c s2), (CRmin_right c s1). 2: apply (CRle_trans _ _ _ H), CRlt_asym, c0. 2: apply CRlt_asym, c0. apply (CRmult_le_reg_l (t1-s1)). apply CRlt_minus, ltst1. rewrite <- CRmult_assoc, <- CRmult_assoc, CRinv_r, CRmult_1_l, CRmult_comm. apply (CRplus_le_reg_r s1). rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRmin_glb. + apply (CRplus_le_reg_r (-s1)). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply (CRmult_le_reg_r (t2-s2)). apply CRlt_minus, ltst2. rewrite CRmult_assoc, CRmult_assoc, CRinv_l, CRmult_1_r. rewrite CRplus_comm, CRmin_plus, CRmult_comm, <- CRmin_mult. 2: apply CRlt_asym, CRlt_minus, ltst1. intro abs. apply CRlt_min in abs. destruct abs. rewrite (CRplus_comm (-s2)) in c2. apply CRmult_lt_reg_r in c2. 2: apply CRlt_minus, ltst2. apply CRplus_lt_reg_r in c2. assert ((t1 - s1) * (- s2 + c) <= (c + - s1) * (t2 - s2)). { clear c1. rewrite CRplus_comm, CRmult_plus_distr_l. rewrite (CRmult_comm (c+-s1)), CRmult_plus_distr_l. apply (AffineLe _ _ _ _ _ s2 t1). do 2 rewrite <- CRmult_plus_distr_l. rewrite CRplus_opp_r, CRmult_0_r. apply CRmult_le_0_compat. apply CRlt_asym, CRlt_minus, ltst2. rewrite <- (CRplus_opp_r s1). apply CRplus_le_compat_r, H. do 2 rewrite <- CRmult_plus_distr_l. rewrite CRmult_comm. apply CRmult_le_compat_r. apply CRlt_asym, CRlt_minus, ltst1. apply CRplus_le_compat_r, H0. split; apply CRlt_asym; assumption. } contradiction. + apply (CRplus_le_reg_r (-s1)). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply (CRmult_le_reg_r (t2-s2)). apply CRlt_minus, ltst2. rewrite CRmult_assoc, CRmult_assoc, CRinv_l, CRmult_1_r. rewrite CRmult_comm. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltst1. apply CRplus_le_compat_r, CRmin_r. - rewrite CRmin_left. 2: apply CRlt_asym, c0. destruct (s s1 c t1 ltst1). + rewrite (CRmin_right c s1). 2: apply CRlt_asym, c1. apply (CRmult_le_reg_l (t1-s1)). apply CRlt_minus, ltst1. rewrite <- CRmult_assoc, <- CRmult_assoc, CRinv_r, CRmult_1_l. apply (CRplus_le_reg_r s1). rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRmin_glb. apply (CRplus_le_reg_r (-s1)). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. rewrite CRmult_comm. apply (CRmult_le_reg_r (t2-s2)). apply CRlt_minus, ltst2. rewrite CRmult_assoc, CRmult_assoc, CRinv_l, CRmult_1_r. setoid_replace (- CRmin c s2) with (-(1) * CRmin c s2). rewrite <- CRmax_min_mult_neg. do 2 rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite CRmax_plus, CRmult_comm, <- CRmax_mult. apply CRmax_lub. rewrite CRplus_opp_r, CRmult_0_r. rewrite <- (CRmult_0_r (c-s1)). apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, c1. apply CRlt_asym, CRlt_minus, ltst2. rewrite CRmult_plus_distr_l, (CRmult_comm (c+-s1)), CRmult_plus_distr_l. apply (AffineLe _ _ _ _ _ s1 t2). do 2 rewrite <- CRmult_plus_distr_l. rewrite CRplus_opp_r, CRmult_0_r. rewrite <- (CRmult_0_r (t1-s1)). apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltst1. rewrite <- (CRplus_opp_r s2). apply CRplus_le_compat_r, H. do 2 rewrite <- CRmult_plus_distr_l. rewrite CRmult_comm. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltst2. apply CRplus_le_compat_r, H0. split; apply CRlt_asym; assumption. apply CRlt_asym, CRlt_minus, ltst1. apply (CRplus_le_reg_l 1). rewrite CRplus_opp_r, CRplus_0_r. apply CRlt_asym, CRzero_lt_one. rewrite <- CRopp_mult_distr_l, CRmult_1_l. reflexivity. apply (CRplus_le_reg_r (-s1)). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. rewrite <- (CRmult_1_r (t1 + - s1)), CRmult_assoc. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltst1. apply (CRmult_le_reg_l (t2-s2)). apply CRlt_minus, ltst2. rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l, CRmult_1_r. apply (CRplus_le_reg_r (CRmin c s2)). rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRmin_plus. apply CRmin_glb. apply (CRplus_le_reg_l s2). rewrite <- CRplus_assoc. apply CRplus_le_compat_r. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRlt_asym, ltst2. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRlt_asym, c0. + clear c0. rewrite (CRmin_left c t1). 2: apply CRlt_asym, c1. apply (CRmult_le_reg_l (t2-s2)). apply CRlt_minus, ltst2. rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l. apply (CRplus_le_reg_l (-c)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. setoid_replace (- CRmin c s2) with (-(1) * CRmin c s2). 2: rewrite <- CRopp_mult_distr_l, CRmult_1_l; reflexivity. rewrite <- CRmax_min_mult_neg. apply CRmax_lub. rewrite <- CRopp_mult_distr_l, CRmult_1_l. apply (CRle_trans _ (-c +0)). rewrite CRplus_0_r; apply CRle_refl. apply CRplus_le_compat_l. apply (CRle_trans _ ((t2-s2)*0)). rewrite CRmult_0_r; apply CRle_refl. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltst2. apply (CRmult_le_reg_l (t1-s1)). apply CRlt_minus, ltst1. rewrite CRmult_0_r, <- CRmult_assoc, CRinv_r, CRmult_1_l. rewrite <- (CRplus_opp_r (CRmin c s1)). apply CRplus_le_compat_r, CRmin_l. rewrite <- CRopp_mult_distr_l, CRmult_1_l. apply (CRplus_le_reg_l c). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l, CRmult_comm. apply (CRmult_le_reg_l (t1-s1)). apply CRlt_minus, ltst1. rewrite <- CRmult_assoc, <- CRmult_assoc, CRinv_r, CRmult_1_l. rewrite CRmult_plus_distr_r. apply (CRplus_le_reg_l (-(c*(t2-s2)))). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite (CRmult_comm (-CRmin c s1)), <- CRopp_mult_distr_r. rewrite <- CRmin_mult. 2: apply CRlt_asym, CRlt_minus, ltst2. rewrite <- CRopp_involutive, CRopp_plus_distr, CRopp_involutive. apply CRopp_ge_le_contravar. intro abs. apply CRlt_min in abs. destruct abs. rewrite <- (CRplus_0_r ((t2-s2)*c)), (CRmult_comm (t2-s2)) in c0. apply CRplus_lt_reg_l in c0. apply (CRplus_lt_compat_l R ((t1 - s1) * (c + - s2))) in c0. rewrite CRplus_opp_r, CRplus_0_r in c0. rewrite <- (CRmult_0_r (t1-s1)) in c0. apply CRmult_lt_reg_l in c0. 2: apply CRlt_minus, ltst1. rewrite <- (CRplus_opp_r s2) in c0. apply CRplus_lt_reg_r in c0. assert ((t2-s2)*s1 <= c * (t2 - s2) + - ((t1 - s1) * (c + - s2))). { apply (CRplus_le_reg_r ((t1 - s1) * (c + - s2))). rewrite CRplus_assoc, CRplus_opp_l, CRplus_comm. rewrite CRmult_plus_distr_l, CRplus_assoc, (CRmult_comm c). apply (AffineLe _ _ _ _ _ s2 t1). 3: split; apply CRlt_asym; assumption. rewrite CRplus_0_r, <- CRplus_assoc, <- CRopp_mult_distr_r. rewrite CRplus_opp_r, CRplus_0_l. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltst2. exact H. rewrite CRplus_0_r, <- CRplus_assoc, <- CRmult_plus_distr_l. apply (CRplus_le_reg_r (-((t2-s2)*s1))). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r, CRopp_mult_distr_r. rewrite <- CRmult_plus_distr_l, CRmult_comm. apply CRmult_le_compat_r. apply CRlt_asym, CRlt_minus, ltst1. apply CRplus_le_compat_r, H0. } contradiction. apply (CRplus_le_reg_l 1). rewrite CRplus_opp_r, CRplus_0_r. apply CRlt_asym, CRzero_lt_one. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia