proposition: Lemma count_occ_sgt l x : l = x :: nil <-> count_occ decA l x = 1 /\ forall y, y <> x -> count_occ decA l y = 0.
proof: Proof. split. - intros ->; cbn; split; intros; destruct decA; subst; intuition. - intros [Heq Hneq]. apply count_occ_repeat_excl in Hneq. rewrite Hneq, count_occ_repeat_eq in Heq; trivial. now rewrite Heq in Hneq. Qed.
imports: PeanoNat