proposition: Lemma a_seq_b_seq_lim : xa [=] xb.
proof: Proof. unfold xa, xb in |- *; clear xa xb. apply cg_inv_unique_2. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. 2: apply Lim_minus. simpl in |- *. apply Limits_unique. simpl in |- *. intros eps H. elim (intervals_small' a b eps H); intros i Hi. exists i; intros. apply AbsIR_imp_AbsSmall. eapply leEq_transitive. 2: apply Hi. eapply leEq_wdl. 2: apply AbsIR_minus. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (a_seq m[-]b_seq m). 2: apply shift_minus_leEq; astepr (b_seq m). 2: apply less_leEq; apply a_seq_less_b_seq. eapply leEq_wdr. 2: apply a_seq_b_seq_dist. rstepl (b_seq m[-]a_seq m). unfold cg_minus in |- *; apply plus_resp_leEq_both. astepl ( [--][--] (b_seq m)); astepr ( [--][--] (b_seq i)). apply inv_resp_leEq; apply local_mon'_imp_mon' with (f := fun n : nat => [--] (b_seq n)); auto. intro; apply inv_resp_leEq; apply b_seq_mon. apply inv_resp_leEq; apply local_mon'_imp_mon'; auto; exact a_seq_mon. Qed.
imports: CoRN.ftc.Continuity