proposition: Lemma cardX (A1 : {pred T1}) (A2 : {pred T2}) : #|[predX A1 & A2]| = #|A1| * #|A2|.
proof: Proof. by rewrite -predX_prod_enum unlock size_filter unlock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)