proposition: Lemma count_predUI a1 a2 s : count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
proof: Proof. elim: s => //= x s IHs; rewrite /= addnACA [RHS]addnACA IHs. by case: (a1 x) => //; rewrite addn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)