proposition: Lemma P_3 : P 3.
proof: Proof. intros n H; rewrite (F_3_eqn (S n)); rewrite iterate_S_eqn. rewrite F_3_eqn. transitivity (exp2 (iterate (F_ 2) (S n) (S n))). - apply PeanoNat.Nat.lt_le_incl; apply exp2_mono. apply iterate_mono; auto. + apply F_alpha_mono. + intro n0; apply (F_alpha_gt (E0fin 2) n0). - specialize (LF2_0 (iterate (F_ 2) (S n) (S n))); intro H0. remember (iterate (F_ 2) (S n) (S n)) as N. transitivity ((fun i : nat => (exp2 i * i)%nat) N). + assert (0 < N). { rewrite HeqN; cbn; apply F_alpha_positive. } rewrite PeanoNat.Nat.mul_comm. destruct (Compat815.mult_O_le (exp2 N) N). auto. * lia. * apply H2. + apply PeanoNat.Nat.lt_le_incl, LF2. Qed.
imports: Coq(Arith) hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) hydras(Compat815)