proposition: Lemma val_qisom Gx : val (qisom Gx) = val Gx.
proof: Proof. by case: (cosetP Gx) => x Nx ->{Gx}; rewrite qisomE /= !val_coset -?eqGH. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)