proposition: Lemma commGC A B : [~: A, B] = [~: B, A].
proof: Proof. rewrite -[[~: A, B]]genV; congr <<_>>; apply/setP=> z; rewrite inE. by apply/imset2P/imset2P=> [] [x y Ax Ay]; last rewrite -{1}(invgK z); rewrite -invg_comm => /invg_inj->; exists y x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)