proposition: Lemma seq_leEq_so_Lim_leEq : forall (seq : CauchySeqR) y, (forall i, seq i [<=] y) -> Lim seq [<=] y.
proof: Proof. intros. rewrite -> leEq_def in |- *. intro H0. generalize (less_Lim_so_less_seq _ _ H0); intro H1. elim H1; intros N H2. pose (c:=H N). rewrite -> leEq_def in c. apply c. apply H2. auto with arith. Qed.
imports: CoRN.reals.CReals Coq(Lia)