proposition: Remark m_eqn : forall k, m k = (l_std alpha k + k)%nat.
proof: Proof. intro k; assert (k <= L_ alpha (S k)). { assert (S k < L_ alpha (S k)). { apply L_ge_S; unfold alpha; intro H0; injection H0. intro; discriminate. } lia. } unfold m,l_std ; 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)