proposition: Lemma In_multiplicity : forall mb a, In a mb -> multiplicity (list_contents B_eq_dec mb) a >= 1.
proof: Proof. intros; induction mb; simpl in *; try tauto. destruct H; destruct (B_eq_dec a0 a); subst; try congruence; simpl; try lia. tauto. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil) CoLoR(ListNodup) CoLoR(ListPermutation)