proposition: Lemma morphpre_gen R : 1 \in R -> R \subset f @* D -> f @*^-1 <<R>> = <<f @*^-1 R>>.
proof: Proof. move=> R1 sRfD; apply/eqP. rewrite eqEsubset andbC gen_subG morphpreS; last exact: subset_gen. rewrite -{1}(morphpreK sRfD) -morphim_gen ?subsetIl // morphimGK //=. by rewrite sub_gen // setIS // preimsetS ?sub1set. by rewrite gen_subG subsetIl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)