proposition: Theorem NoDup_count_occ l: NoDup l <-> (forall x:A, count_occ decA l x <= 1).
proof: Proof. induction l as [| a l' Hrec]. - simpl; split; auto. constructor. - rewrite NoDup_cons_iff, Hrec, (count_occ_not_In decA). clear Hrec. split. + intros (Ha, H) x. simpl. destruct (decA a x); auto. subst; now rewrite Ha. + intro H; split. * specialize (H a). rewrite count_occ_cons_eq in H; trivial. now inversion H. * intros x. specialize (H x). simpl in *. destruct (decA a x); auto. now apply Nat.lt_le_incl. Qed.
imports: PeanoNat