proposition: Theorem NoDup_count_occ' l: NoDup l <-> (forall x:A, In x l -> count_occ decA l x = 1).
proof: Proof. rewrite NoDup_count_occ. setoid_rewrite (count_occ_In decA). unfold gt, lt in *. split; intros H x; specialize (H x); set (n := count_occ decA l x) in *; clearbody n. - now apply Nat.le_antisymm. - destruct (Nat.le_gt_cases 1 n); trivial. + rewrite H; trivial. + now apply Nat.lt_le_incl. Qed.
imports: PeanoNat