proposition: Lemma LF1' : forall i j, exp2 i * j < iterate (F_ 1) (S i) j .
proof: Proof. induction i. - cbn. intros; cbn. ring_simplify. rewrite LF0'. lia. - intros. simpl exp2. ring_simplify. simpl (2+i). rewrite iterate_S_eqn. rewrite LF1. specialize (IHi j). rewrite <- Nat.mul_assoc. generalize IHi; generalize (exp2 i * j); generalize (iterate (F_ 1) (S i) j). clear IHi. intros. lia. Qed.
imports: Coq(ArithRing Lia Arith)