proposition: Lemma count_occ_unique x l : count_occ decA l x = length l -> l = repeat x (length l).
proof: Proof. induction l as [|h l]; cbn; intros Hocc; auto. destruct (decA h x). - f_equal; intuition. - assert (Hb := count_occ_bound decA x l). rewrite Hocc in Hb. exfalso; apply (Nat.nle_succ_diag_l _ Hb). Qed.
imports: PeanoNat