proposition: Lemma ins_meq_union M N P a : M + {{a}} =mul= N + P -> a in N -> M =mul= N - {{a}} + P.
proof: Proof. mset_unfold; try_solve_meq. assert (((x/M)%msets + (x/{{a}})%msets)%nat = ((x/N)%msets + (x/P)%msets)%nat). rewrite <- !union_mult. apply meq_multeq; trivial. case (eqA_dec x a); intro x_a. assert (x/N = a/N). apply mult_eqA_compat; trivial. rewrite singleton_mult_in. assert (((x/M)%msets + 1)%nat = ((x/N)%msets + (x/P)%msets)%nat). rewrite <- (singleton_mult_in x_a); trivial. lia. trivial. rewrite (singleton_mult_notin x_a). assert (((x/M)%msets + 0)%nat = ((x/N)%msets + (x/P)%msets)%nat). rewrite <- (singleton_mult_notin x_a); trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)