proposition: Remark R00 : F_ alpha >> fun n => Ack n n.
proof: Proof. destruct (F_mono_l alpha E0_omega Halpha) as [N HN]; exists (Nat.max N 2); intros p Hp. apply Nat.le_lt_trans with (F_ E0_omega p). - apply F_vs_Ack; auto; lia. - apply HN; lia. Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)