proposition: Lemma sub_morphpre_im R G : 'ker f \subset G -> G \subset D -> R \subset f @* D -> (f @*^-1 R \subset G) = (R \subset f @* G).
proof: Proof. by symmetry; rewrite -morphpreSK ?morphimGK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)