proposition: Lemma noext_big: forall a M N, M >mul N -> (forall m, m in M -> a >A m) -> (forall n, n in N -> a >A n).
proof: Proof. intros a m n MN; induction MN; intros. inversion H. assert (n in (X+Y)); [rewrite <- H3; trivial | idtac]. case (member_union H5); intro nIn. apply H0. rewrite H2; unfold insert; auto with multisets. assert (a >A a0). apply H0. rewrite H2; auto with multisets. assert (a0 >A n). apply H4; auto with multisets. eauto with sets. apply IHMN2; trivial. apply IHMN1; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)