proposition: Theorem every_battle_terminates : Termination.
proof: Proof. red; apply Inclusion.wf_incl with (R2 := fun h h' => m h t1< m h'). red; intros; now apply round_decr. apply Inverse_Image.wf_inverse_image, T1_wf. Qed.
imports: hydras(E0 Hessenberg)