proposition: Lemma gFsub_trans gT (G : {group gT}) (A : {pred gT}) : G \subset A -> F gT G \subset A.
proof: Proof. exact/subset_trans/gFsub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)