proposition: Lemma quotmE x : x \in G -> quotm (coset H x) = coset (f @* H) (f x).
proof: Proof. exact: factmE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)