proposition: Lemma Lim_less_Lim_so_seq_less_seq : forall seq1 seq2 : CauchySeq IR, Lim seq1 [<] Lim seq2 -> {N : nat | forall m, N <= m -> seq1 m [<] seq2 m}.
proof: Proof. intros. set (Av := (Lim seq1[+]Lim seq2) [/]TwoNZ) in |- *. cut (Lim seq1 [<] Av); try intro H0. cut (Av [<] Lim seq2); try intro H1. generalize (Lim_less_so_seq_less _ _ H0); intro H2. generalize (less_Lim_so_less_seq _ _ H1); intro H3. elim H2; intro N1; intro H4. elim H3; intro N2; intro H5. exists (Nat.max N1 N2); intros. apply less_leEq_trans with Av. apply H4. apply Nat.le_trans with (Nat.max N1 N2). apply Nat.le_max_l. assumption. apply less_leEq. apply H5. apply Nat.le_trans with (Nat.max N1 N2). apply Nat.le_max_r. assumption. unfold Av in |- *. apply Average_less_Greatest. assumption. unfold Av in |- *. apply Smallest_less_Average. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)