proposition: Lemma mord_meq_compat mA mA' mB mB' : mA =mul= mA' -> mB =mul= mB' -> mA >mul mB -> mA' >mul mB'.
proof: Proof. intros. rewrite <- H, <- H0; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)