proposition: Lemma morphpre_set1 x : x \in D -> f @*^-1 [set f x] = 'ker f :* x.
proof: Proof. by move=> Dx; rewrite -morphim_set1 // morphimK ?sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)