proposition: Lemma mult_remove_in : forall x a M, x =A= a -> (x / (rem a M))%msets = ((x / M)%msets - 1)%nat.
proof: Proof. induction M. auto. intro x_a. simpl; destruct (eqA_dec x a0); destruct (eqA_dec a a0); simpl; try solve [absurd (x =A= a); eauto with sets]. auto with arith. destruct (eqA_dec x a0). contr. auto. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)