proposition: Lemma L2 : forall n, 2 <= n -> forall p, 2 <= p -> Ack n p <= F_ n p.
proof: Proof. induction 1. - intros; rewrite Ack_2_n; transitivity (exp2 p * p). + apply L02; auto. + apply PeanoNat.Nat.lt_le_incl; apply LF2. - intros; apply L; auto. Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)