proposition: Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x.
proof: Proof. have [/perm_to_rem/permP->|xNs]/= := boolP (x \in s); first by rewrite addKn. by rewrite subn0 rem_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)