proposition: Remark m_dominates_Ack_from_3 : forall n, 3 <= n -> Ack n n <= m n.
proof: Proof. destruct n. - lia. - intro; apply m_ge_Ack; 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)