proposition: Lemma memJ_class_support A B x y : x \in A -> y \in B -> x ^ y \in class_support A B.
proof: Proof. by move=> Ax By; apply: imset2_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)