proposition: Lemma rounds_trans {B:Battle} : forall i h j h', rounds B i h j h' -> forall k h0, rounds B k h0 i h -> rounds B k h0 j h'.
proof: Proof. intros i h j h' H k h0. induction 1 /dr. - intros h'0 ? ?; now right with h'0. - intros ? ? ? h'' ? ? ? ; right with h'';auto. 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)