proposition: Theorem every_battle_terminates : Termination.
proof: Proof. red; apply Inclusion.wf_incl with (R2 := fun h h' => LT (m h) (m h')). - case mVariant => Hvar; rewrite /inclusion => x y Hstep. case: Hstep => x0 Hstep; apply (Hvar x0 y x). move => Hhead; subst; apply (head_no_round_n _ _ Hstep). by [exists x0]. - apply Inverse_Image.wf_inverse_image, nf_Wf. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic) hydras(T1 E0 Hessenberg Hydra_Theorems Hydra_Definitions Hydra_Termination Battle_length Hydra_Examples Epsilon0_Needed_Free Epsilon0_Needed_Std) T1Bridge GHessenberg GL_alpha GPrelude