proposition: Lemma rounds_free_equiv1 : forall i j h h', rounds free i h j h' -> h -+-> h'.
proof: Proof. induction 1. - now left. - now right with 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)