proposition: Lemma injmP : reflect {in D &, injective f} ('injm f).
proof: Proof. apply: (iffP subsetP) => [injf x y Dx Dy | injf x /= Kx]. by case/ker_rcoset=> // z /injf/set1P->; rewrite mul1g. have Dx := dom_ker Kx; apply/set1P/injf => //. by apply/rcoset_kerP; rewrite // mulg1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)