proposition: Lemma standard_incl_free : forall i h h', battle_rel standard i h h'-> battle_rel free i h h' .
proof: Proof. - intros; red. red in H. now exists i. 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)