proposition: Lemma leEq_seq_so_leEq_Lim : forall (seq : CauchySeqR) y, (forall i, y [<=] seq i) -> y [<=] Lim seq.
proof: Proof. intros. rewrite -> leEq_def in |- *. intro H0. generalize (Lim_less_so_seq_less _ _ 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)