proposition: Lemma CR_cv_open_below : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (m l : CRcarrier R), CR_cv R un l -> m < l -> { n : nat & forall i:nat, le n i -> m < un i }.
proof: Proof. intros. apply CRlt_minus in H0. pose proof (Un_cv_nat_real _ l H (l-m) H0) as [n nmaj]. exists n. intros. specialize (nmaj i H1). apply CRabs_lt in nmaj. destruct nmaj as [_ nmaj]. unfold CRminus in nmaj. rewrite CRopp_plus_distr, CRopp_involutive, CRplus_comm in nmaj. apply CRplus_lt_reg_l in nmaj. apply (CRplus_lt_reg_l R (-m)). rewrite CRplus_opp_l. apply (CRplus_lt_reg_r (-un i)). rewrite CRplus_0_l. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. exact nmaj. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs