proposition: Lemma ker_normal_pre M : 'ker f <| f @*^-1 M.
proof: Proof. by rewrite /normal ker_sub_pre subIset ?ker_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)