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