proposition: Lemma sub_im_coset (C : {set coset_of}) : C \subset coset @* 'N(A).
proof: Proof. by rewrite im_coset subsetT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)