proposition: Lemma tuto_count_filter : forall s, count a s = size (filter a s).
proof: Proof. by elim=> [|x s IHs] //=; rewrite IHs; case (a x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)