fact: Definition rgd_fun (p : {perm T'}) := [fun x1 => if insub x1 is Some u then sval (p u) else x].
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)