proposition: Lemma acc_mord : forall M, AccM M -> (forall x, x in M -> AccA x).
proof: Proof. intros M acc_M. induction acc_M as [M acc_M IHM]. intros x x_in_M. constructor. intros y y_less_x. apply (IHM (M - {{x}} + {{y}})); auto with multisets. constructor. apply MSetRed with (X := M - {{x}}) (a := x) (Y := {{y}}); auto with multisets. intros y0 Hy0. gen (member_singleton Hy0); clear Hy0; intro Hy0. eapply gtA_eqA_compat. refl. sym. apply Hy0. hyp. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)