proposition: Corollary LF2' : forall i, 1 <= i -> exp2 i < F_ 2 i.
proof: Proof. intros; apply Nat.le_lt_trans with (exp2 i * i). - destruct (Compat815.mult_O_le (exp2 i) i). + lia. + now rewrite Nat.mul_comm. - apply LF2. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)