proposition: Lemma kercoset_rcoset x y : x \in 'N(H) -> y \in 'N(H) -> coset H x = coset H y -> exists2 z, z \in H & x = z * y.
proof: Proof. by move=> Nx Ny eqfxy; rewrite -ker_coset; apply: ker_rcoset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)