proposition: Lemma eq_in_count s : {in s, a1 =1 a2} -> count a1 s = count a2 s.
proof: Proof. by move/eq_in_filter=> eq_a12; rewrite -!size_filter eq_a12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)