proposition: Lemma diff_mult : forall M N x, x / (M - N) = ((x / M)%msets - (x / N)%msets)%nat.
proof: Proof. induction N. simpl; intros; lia. intro x; simpl. destruct (eqA_dec x a); simpl. fold rem. rewrite (diff_mult_step_eq M N e). rewrite (IHN x). lia. fold rem. rewrite (diff_mult_step_neq M N n). exact (IHN x). Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)