proposition: Lemma mult_insert : forall M a, (a/(M + {{a}}))%msets > 0.
proof: Proof. intros M a. replace (a/(M + {{a}})) with ((a/M)%msets + (a/{{a}})%msets)%nat. replace (a/{{a}}) with 1. lia. sym; auto with multisets sets. auto with multisets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)