proposition: Lemma classM x A B : x ^: (A * B) = class_support (x ^: A) B.
proof: Proof. by rewrite -!class_support_set1l class_supportM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)