proposition: Lemma injm_comp : 'injm f -> 'injm g -> 'injm gof.
proof: Proof. by move=> injf; rewrite ker_comp; move/trivgP=> ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)