proposition: Lemma LF2 : forall i, exp2 i * i < F_ 2 i.
proof: Proof. intro i; ochange (E0fin 2) (E0_succ 1); rewrite F_succ_eqn. undiag2 i 1 3. - intros. cbn; intros; cbn. repeat rewrite LF1. abstract lia. - intros; simpl exp2; ring_simplify. simpl (2+n)%nat. rewrite iterate_S_eqn, LF1; abstract lia. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)