proposition: Lemma tuto_count_predUI : forall a1 a2 s, count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
proof: Proof. move=> a1 a2. elim=> [|x s IHs] //=. rewrite addnCA -addnA addnA addnC IHs -!addnA. nat_congr. nat_congr. by case (a1 x); case (a2 x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)