proposition: Lemma class_supportM A B C : class_support A (B * C) = class_support (class_support A B) C.
proof: Proof. apply/setP=> x; apply/imset2P/imset2P=> [[a y Aa] | [y c]]. case/mulsgP=> b c Bb Cc -> ->{x y}. by exists (a ^ b) c; rewrite ?(imset2_f, conjgM). case/imset2P=> a b Aa Bb -> Cc ->{x y}. by exists a (b * c); rewrite ?(mem_mulg, conjgM). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)