proposition: Lemma predX_prod_enum (A1 : {pred T1}) (A2 : {pred T2}) : count [predX A1 & A2] prod_enum = #|A1| * #|A2|.
proof: Proof. rewrite !cardE !size_filter -!enumT /prod_enum. elim: (enum T1) => //= x1 s1 IHs; rewrite count_cat {}IHs count_map /preim /=. by case: (x1 \in A1); rewrite ?count_pred0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)