proposition: Lemma mord_ext1_aux: forall a X Y, a in X -> a in Y -> (forall y, y in Y -> (exists2 x, x in X & x >A y)) -> (forall y, y in (Y - {{a}}) -> (exists2 x, x in (X - {{a}}) & x >A y)).
proof: Proof. intros; destruct (H1 y). eauto with multisets. case (eqA_dec a x); intro ax. destruct (H1 a). eauto with multisets. exists x0; try apply mem_memrem; eauto with sets. exists x; solve [apply mem_memrem; auto with sets | trivial]. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)