proposition: Lemma diff_mult_comp : forall x N M M', M =mul= M' -> x / (M - N) = x / (M' - N).
proof: Proof. induction N. intros; apply meq_multeq; trivial. intros M M' MM'. simpl. apply IHN. apply multeq_meq. intro x'. case (eqA_dec x' a). intro xa; rewrite !mult_remove_in; trivial. rewrite (meq_multeq MM'); trivial. intro xna; rewrite !mult_remove_not_in; trivial. apply meq_multeq; trivial. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)