proposition: Lemma seq_is_CC_Cauchy : forall s, (forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) -> CC_Cauchy_prop s.
proof: Proof. unfold CC_Cauchy_prop in |- *. split. unfold Cauchy_prop in |- *. intros e zlte. generalize (N_exists nrtq zlt_nrtq nrtqlt1 nrtc zlt_nrtc e zlte). intro Hex. elim Hex. intros N HN. exists N. intros m leNm. apply AbsIR_imp_AbsSmall. generalize (SublemmaRe s H N m leNm). intro H2. generalize (HN m leNm). intro H3. eapply leEq_transitive. 2: apply H3. rstepr ((nrtq[^]m[-]nrtq[^]N[/] nrtq[-][1][//]nrtq_) [*]nrtc). exact H2. unfold Cauchy_prop in |- *. intros e zlte. generalize (N_exists nrtq zlt_nrtq nrtqlt1 nrtc zlt_nrtc e zlte). intro Hex. elim Hex. intros N HN. exists N. intros m leNm. apply AbsIR_imp_AbsSmall. generalize (SublemmaIm s H N m leNm). intro H2. generalize (HN m leNm). intro H3. eapply leEq_transitive. 2: apply H3. rstepr ((nrtq[^]m[-]nrtq[^]N[/] nrtq[-][1][//]nrtq_) [*]nrtc). exact H2. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)