proposition: Lemma Rsmaller_interval : forall {R : ConstructiveReals} (a b c d : CRcarrier R), a <= c -> c <= b -> a <= d -> d <= b -> CRabs _ (d - c) <= b-a.
proof: Proof. intros. apply CRabs_le. split. - apply (CRplus_le_reg_l (c+b)). unfold CRminus. rewrite CRopp_plus_distr. rewrite CRplus_assoc, <- (CRplus_assoc b). rewrite CRplus_opp_r, (CRplus_comm c b), CRplus_assoc. apply CRplus_le_compat. exact H0. rewrite CRopp_involutive, CRplus_0_l, CRplus_comm. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. exact H1. - apply (CRplus_le_reg_r (a+c)). unfold CRminus. rewrite (CRplus_assoc b), <- (CRplus_assoc (-a)). rewrite CRplus_opp_l, CRplus_0_l, CRplus_assoc. apply CRplus_le_compat. exact H2. rewrite CRplus_comm. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. exact H. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal