proposition: Lemma LF3_2 : dominates_from 2 (F_ 3) (fun n => iterate exp2 (S n) n).
proof: Proof. intros p H; assert (H0:= LF2_0). ochange (E0fin 3) (E0_succ 2); rewrite F_succ_eqn. eapply iterate_dom_prop; eauto with arith. - apply exp2_ge_S. - apply exp2_mono. - apply F_alpha_mono. - red; intros; transitivity (exp2 p0 * p0)%nat; auto. { rewrite <- Nat.mul_1_r at 1; apply Nat.mul_lt_mono_pos_l; auto. apply exp2_positive. } apply LF2_0; abstract lia. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)