proposition: Lemma standard_battle_head : forall i h j h', @rounds standard i h j h' -> h <> head.
proof: Proof. induction 1; intro; subst h; eapply head_no_round_n ; eauto. 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)