proposition: Lemma N_exists : {N : nat | forall m, N <= m -> (q[^]m[-]q[^]N[/] q[-][1][//]q_) [*]c [<=] e}.
proof: Proof. cut ([0] [<] [1][-]q). intro H0. cut ([1][-]q [#] [0]). intro H3. cut (c [#] [0]). intro H1. cut ([0] [<] ([1][-]q) [*] (e[/] c[//]H1)). intro H2. elim (qi_yields_zero q zleq qlt1 (([1][-]q) [*] (e[/] c[//]H1)) H2). intros N HN. exists N. intros m leNm. rstepl ((q[^]N[-]q[^]m[/] [1][-]q[//]H3) [*]c). apply shift_mult_leEq with H1. assumption. apply shift_div_leEq'. assumption. apply leEq_transitive with (q[^]N). rstepl ([0][+] (q[^]N[-]q[^]m)). apply shift_plus_leEq. rstepr (q[^]m). apply nexp_resp_nonneg. assumption. assumption. apply mult_resp_pos. assumption. apply div_resp_pos. assumption. assumption. apply ap_symmetric_unfolded. apply less_imp_ap. assumption. apply ap_symmetric_unfolded. apply less_imp_ap. assumption. apply shift_less_minus. rstepl q. assumption. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)