proposition: Lemma rounds_free_equiv2 : forall h h', h -+-> h' -> forall i, exists j, rounds free i h j h'.
proof: Proof. induction 1 as [h h' H | h h'' h' H H0 Hind]. - intro i; exists (S i); left;auto. - intros i. destruct (Hind (S i)) as [j Hj]. exists j; eright; 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)