proposition: Lemma m_strict_mono {A:Type} {Lt: relation A}{St: StrictOrder Lt} {Wf: well_founded Lt} m (V: @Hvariant _ _ Wf free m){h h':Hydra}: h -+-> 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 y); 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)