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