proposition: Lemma imset_coset G : coset H @: G = G / H.
proof: Proof. apply/eqP; rewrite eqEsubset andbC imsetS ?subsetIr //=. apply/subsetP=> _ /imsetP[x Gx ->]. by case Nx: (x \in 'N(H)); rewrite ?(coset_default Nx) ?mem_morphim ?group1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)