proposition: Lemma count_occ_repeat_excl x l : (forall y, y <> x -> count_occ decA l y = 0) -> l = repeat x (length l).
proof: Proof. intros Hocc. apply Forall_eq_repeat, Forall_forall; intros z Hin. destruct (decA z x) as [Heq|Hneq]; auto. apply Hocc, count_occ_not_In in Hneq; intuition. Qed.
imports: PeanoNat