proposition: Lemma commg_sub A B : [~: A, B] \subset A <*> B.
proof: Proof. by rewrite comm_subG // (joing_subl, joing_subr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)