proposition: Lemma mkerl x y : x \in 'ker f -> y \in D -> f (x * y) = f y.
proof: Proof. by move=> Kx Dy; rewrite morphM // ?(dom_ker, mker Kx, mul1g). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)