proposition: Lemma Lim_leEq_Lim : forall seq1 seq2 : CauchySeqR, (forall i, seq1 i [<=] seq2 i) -> Lim seq1 [<=] Lim seq2.
proof: Proof. intros. rewrite -> leEq_def in |- *. intro H0. generalize (Lim_less_Lim_so_seq_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)