proposition: Lemma multiplicity_NoDupA : forall l, NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
proof: Proof. induction l. - simpl. split; auto with arith. - split; simpl. + inversion_clear 1. rewrite IHl in H1. intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *. rewrite <- EQ. rewrite multiplicity_InA_O; auto. + intros; constructor. * rewrite multiplicity_InA. specialize (H a). rewrite if_eqA_refl in H. clear IHl; lia. * rewrite IHl; intros. specialize (H a0). lia. Qed.
imports: Lia Relations Multiset SetoidList