proposition: Lemma mem_commg A B x y : x \in A -> y \in B -> [~ x, y] \in [~: A, B].
proof: Proof. by move=> Ax By; rewrite mem_gen ?imset2_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)