proposition: Lemma rgdP p : injective (rgd_fun p).
proof: Proof. apply: can_inj (rgd_fun p^-1) _ => y /=. case: (insubP _ y) => [u _ val_u|]; first by rewrite valK permK. by rewrite negbK; move/eqP->; rewrite insubF //= eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype tuple tuple bigop prime finset fingroup) mathcomp(morphism perm automorphism quotient action cyclic) mathcomp(pgroup gseries sylow primitive_action)