proposition: Lemma Main_2' : forall (t : IR) (i k : nat), a i[*] (t[*]p3m 0) [^]i[-]eps [<=] a k[*] (t[*]p3m 0) [^]k -> a i[*]t[^]i[-]eps [<=] a k[*]t[^]k.
proof: Proof. intros. cut (t[*]p3m 0 [=] t). intro. astepl (a i[*] (t[*]p3m 0) [^]i[-]eps). astepr (a k[*] (t[*]p3m 0) [^]k). auto. Step_final (t[*][1]). Qed.
imports: CoRN.reals.CSumsReals CoRN.fta.KeyLemma CoRN.algebra.CRing_as_Ring Coq(Lia)