proposition: Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y).
proof: Proof. rewrite count_rem; have []//= := boolP (x \in s). by case: eqP => // <- /count_memPn->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)