proposition: Lemma CR_cv_open_above : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (m l : CRcarrier R), CR_cv R un l -> l < m -> { n : nat & forall i:nat, le n i -> un i < m }.
proof: Proof. intros. apply CRlt_minus in H0. pose proof (Un_cv_nat_real _ l H (m-l) H0) as [n nmaj]. exists n. intros. specialize (nmaj i H1). apply CRabs_lt in nmaj. destruct nmaj as [nmaj _]. apply CRplus_lt_reg_r in nmaj. exact nmaj. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs