proposition: Lemma Main_2 : forall (t : IR) (j k : nat), let r := t[*]p3m j in [0] [<=] t -> a k[*]t[^]k [=] a_0[-]eps -> (forall i, 1 <= i -> i <= n -> a i[*]t[^]i[-]eps [<=] a k[*]t[^]k) -> forall i, 1 <= i -> i <= n -> a i[*]r[^]i [<=] a_0.
proof: Proof. intros. unfold r in |- *. apply leEq_transitive with (a i[*]t[^]i). astepl (a i[*] (t[^]i[*]p3m j[^]i)). rstepl (p3m j[^]i[*] (a i[*]t[^]i)). astepr ([1][*] (a i[*]t[^]i)). apply mult_resp_leEq_rht. astepr ([1][^]i:IR). apply nexp_resp_leEq. apply less_leEq; apply p3m_pos. apply p3m_small. astepl ([0][*]t[^]i). apply mult_resp_leEq_rht; auto. astepl ([0][^]i:IR). apply nexp_resp_leEq; auto. apply leEq_reflexive. apply leEq_wdr with (eps[+]a k[*]t[^]k). apply shift_leEq_plus'; auto. astepl (eps[+] (a_0[-]eps)); rational. Qed.
imports: CoRN.reals.CSumsReals CoRN.fta.KeyLemma CoRN.algebra.CRing_as_Ring Coq(Lia)