proposition: Lemma variant_mono_free {A:Type} {Lt: relation A}{Tr : Transitive Lt} {Wf: well_founded Lt} m {V: Hvariant Wf free m}: forall i h j h', rounds free i h j h' -> Lt (m h') (m h).
proof: Proof. induction 1;auto. - apply (variant_decr 0). + intro; subst; eapply head_no_round; eauto. + auto. - transitivity (m h''); auto. apply (variant_decr 0). + intro; subst; eapply head_no_round; eauto. + 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)