proposition: Lemma gFsub gT (G : {group gT}) : F gT G \subset G.
proof: Proof. by case: F gT G. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)