proposition: Lemma F_vs_Ack n : 2 <= n -> Ack n n <= F_ E0_omega n.
proof: Proof. intros; rewrite F_lim_eqn. - rewrite Canon.Canon_Omega; apply L2; auto. - reflexivity. Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)