proposition: Lemma injm1 x : x \in D -> f x = 1 -> x = 1.
proof: Proof. by move=> Dx; move/(kerP Dx); rewrite ker_injm; move/set1P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)