proposition: Remark m_dominates_Ack : dominates (fun n => S (m n)) (fun n => Ack.Ack n n).
proof: Proof. exists 3; red; intros. apply Nat.le_lt_trans with (m p). - apply m_dominates_Ack_from_3; auto. - auto with arith. 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)