proposition: Theorem count_occ_inv_nil l : (forall x:A, count_occ l x = 0) <-> l = [].
proof: Proof. split. - induction l as [|x l]; trivial. intros H. specialize (H x). simpl in H. destruct eq_dec as [_|NEQ]; [discriminate|now elim NEQ]. - now intros ->. Qed.
imports: PeanoNat