proposition: Lemma CC_SeqLimit_uniq : forall (s : nat -> CC) (l l' : CC), CC_SeqLimit s l -> CC_SeqLimit s l' -> l [=] l'.
proof: Proof. unfold CC_SeqLimit in |- *. do 3 intro. intros H H0. apply cg_inv_unique_2. apply AbsCC_small_imp_eq. intros e H1. cut ([0] [<] e [/]ThreeNZ). intro H2. elim (H (e [/]ThreeNZ)). intro N. intros H3. elim (H0 (e [/]ThreeNZ)). intro N'. intros H4. cut {M : nat | N <= M | N' <= M}. intros H5. elim H5. clear H5. intro M. intros. apply leEq_less_trans with (AbsCC (s M[-]l) [+]AbsCC (s M[-]l')). apply leEq_wdl with (AbsCC ( [--] (s M[-]l) [+] (s M[-]l'))). apply leEq_wdr with (AbsCC [--] (s M[-]l) [+]AbsCC (s M[-]l')). apply triangle. algebra. apply AbsCC_wd. rational. rstepr (e [/]ThreeNZ[+]e [/]ThreeNZ[+]e [/]ThreeNZ). astepl ([0][+]AbsCC (s M[-]l) [+]AbsCC (s M[-]l')). apply plus_resp_less_leEq. apply plus_resp_less_leEq. auto. apply H3. auto. apply H4. auto. exists (Nat.max N N'); auto with arith. auto. auto. apply pos_div_three. auto. Qed.
imports: CoRN.complex.AbsCC Coq(Lia)