proposition: Lemma maxin_not_lt: forall M N, M >mul N -> {x:A | x in N & (forall y, y in M -> x >A y)} -> False.
proof: Proof. intros M N MN cond; destruct cond. absurd (x >A x); auto with sets. apply (noext_big MN g m). Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)