proposition: Lemma multiplicity_nodup : forall mb, (forall a, multiplicity (list_contents B_eq_dec mb) a <= 1) -> nodup mb.
proof: Proof. intros. induction mb; simpl; auto. simpl in H. split. ded (H a). intuition. ded (In_multiplicity _ _ H1). destruct (B_eq_dec a a); auto. lia. apply IHmb. intros. ded (H a0). destruct (B_eq_dec a a0); simpl in *; lia. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil) CoLoR(ListNodup) CoLoR(ListPermutation)