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