proposition: Lemma Termination_strong (B:Battle) : Termination -> B_termination B.
proof: Proof. intro H; red; apply wf_incl with (R2:=(transp _ round)). - intros h' h; destruct 1 as [i Hi]; now generalize (battle_ok _ _ _ Hi). - apply H. Qed.
imports: Coq(Arith Lia List Relation_Operators Operators_Properties Peano_dec Wellfounded.Inverse_Image Wellfounded.Inclusion) hydras(More_Arith Epsilon0 Hessenberg Simple_LexProd MoreLibHyps)