proposition: Lemma L2 : exp2 (F_ (E0_succ alpha) n) <= (F_ (E0_succ alpha) (S n)).
proof: Proof. assert (H: 2 <= (F_ (E0_succ alpha) n)). { apply Nat.le_lt_trans with n. - lia. - apply F_alpha_gt. } assert (H0: F_ (E0_succ alpha) n < iterate (F_ alpha) (S n) (S n)). { rewrite F_succ_eqn; apply iterate_mono; auto. - apply F_alpha_mono. - intro; apply F_alpha_gt. } generalize(R1 (F_ (E0_succ alpha) n) H (iterate (F_ alpha) (S n) (S n)) H0); intro H1; rewrite <- R3 in H1. transitivity ( exp2 (F_ alpha (F_ (E0_succ alpha) n))); [| auto]. - apply PeanoNat.Nat.lt_le_incl; apply exp2_mono. apply F_alpha_gt. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)