proposition: Lemma L: forall p, 2 <= p -> Ack (S n) p <= F_ (S n) p.
proof: Proof. intros p Hp; destruct p. - lia. - rewrite Ack_iterate_rw; rewrite F_iterate_rw. transitivity (iterate (Ack n) (S (S p)) (S p)). + apply iterate_mono2. * apply Ack_mono_r. * lia. + eapply iterate_mono_1; auto. * apply Ack_strict_mono. * apply le_S_Ack. * intros; apply Hn; eauto with arith. Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)