proposition: Remark m_ge_F_omega k: F_ E0_omega (S k) <= m (S k).
proof: Proof. rewrite m_eqn; transitivity (H'_ alpha (S k)). - apply H'_F. - unfold l_std; generalize (H'_L_ alpha (S k)); lia. 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)