proposition: Lemma rcoset_kerP x y : x \in D -> y \in D -> reflect (f x = f y) (x \in 'ker f :* y).
proof: Proof. move=> Dx Dy; rewrite mem_rcoset !inE groupM ?morphM ?groupV //=. by rewrite morphV // -eq_mulgV1; apply: eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)