proposition: Lemma LF3 : dominates_from 2 (F_ 3) (fun n => iterate exp2 n n).
proof: Proof. generalize (LF3_2); intros H n Hn; eapply Nat.le_lt_trans. - apply iterate_le_n_Sn; intro x; generalize (exp2_gt_id x); lia. - now apply H. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)