proposition: Lemma injm_factmP : reflect ('ker f = 'ker q) ('injm ff).
proof: Proof. rewrite ker_factm -morphimIdom sub_morphim_pre ?subsetIl //. rewrite setIA (setIidPr sGH) (sameP setIidPr eqP) (setIidPl _) // eq_sym. exact: eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)