proposition: Remark m_ge_Ack: forall n, 2 <= n -> Ack (S n) (S n) <= m (S n).
proof: Proof. intros n H0; transitivity (F_ E0_omega (S n)). - apply F_vs_Ack; auto. - apply m_ge_F_omega. Qed.
imports: hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination L_alpha Battle_length Ack) hydras(primRec F_alpha AckNotPR PrimRecExamples F_omega)