proposition: Lemma Main_3a : forall (t : IR) (j k k_0 : nat), let r := t[*]p3m j in k_0 <= n -> a k_0[*]t[^]k_0 [=] a_0[-]eps -> a k_0[*]r[^]k_0[-]eps [<=] a k[*]r[^]k -> p3m (j * n) [*]a_0[-]Two[*]eps [<=] a k[*]r[^]k.
proof: Proof. intros. unfold r in |- *. rstepl (p3m (j * n) [*]a_0[-]eps[-]eps). apply leEq_transitive with (a k_0[*] (t[*]p3m j) [^]k_0[-]eps); auto. apply minus_resp_leEq. astepr (a k_0[*] (t[^]k_0[*]p3m j[^]k_0)). astepr (a k_0[*] (t[^]k_0[*]p3m (j * k_0))). rstepr (p3m (j * k_0) [*] (a k_0[*]t[^]k_0)). astepr (p3m (j * k_0) [*] (a_0[-]eps)). astepr (p3m (j * k_0) [*]a_0[-]p3m (j * k_0) [*]eps). apply minus_resp_leEq_both. apply mult_resp_leEq_rht. apply p3m_mon'; auto with arith. apply less_leEq; apply a_0_pos. astepr ([1][*]eps). apply mult_resp_leEq_rht. apply p3m_small. apply less_leEq; auto. Qed.
imports: CoRN.reals.CSumsReals CoRN.fta.KeyLemma CoRN.algebra.CRing_as_Ring Coq(Lia)