proposition: Theorem battle_length_std_Hardy (alpha : E0) : alpha <> E0zero -> forall k , 1 <= k -> exists l: nat, H'_ alpha k - k <= l /\ battle_length standard k (iota (cnf alpha)) l.
proof: Proof. intros H k H0; exists (L_ alpha (S k) - k); split. - generalize (H'_L_ alpha k); lia. - now apply battle_length_std. Qed.
imports: hydras(Hydra_Lemmas Epsilon0_Needed_Free Epsilon0_Needed_Std Hydra_Termination L_alpha Battle_length Ack)