proposition: Lemma injm_ifactm : 'injm g -> 'injm ifactm.
proof: Proof. by rewrite ker_ifactm => /trivgP->; rewrite morphim1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)