proposition: Lemma CR_cv_le : forall {R : ConstructiveReals} (u v : nat -> CRcarrier R) (a b : CRcarrier R), (forall n:nat, u n <= v n) -> CR_cv R u a -> CR_cv R v b -> a <= b.
proof: Proof. intros. apply (CRplus_le_reg_r (-a)). rewrite CRplus_opp_r. apply (CR_cv_bound_down (fun i:nat => v i - u i) _ _ 0). - intros. rewrite <- (CRplus_opp_l (u n)). unfold CRminus. rewrite (CRplus_comm (v n)). apply CRplus_le_compat_l. apply H. - apply CR_cv_plus. + exact H1. + apply CR_cv_opp, H0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs