proposition: Lemma ker_rcoset x y : x \in D -> y \in D -> f x = f y -> exists2 z, z \in 'ker f & x = z * y.
proof: Proof. by move=> Dx Dy eqfxy; apply/rcosetP; apply/rcoset_kerP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)