proposition: Lemma rfdP p : injective (rfd_fun p).
proof: Proof. apply: can_inj (rfd_fun p^-1) _ => u; apply: val_inj => /=. rewrite -(can_eq (permK p)) permKV eq_sym. by case: eqP => _; rewrite !(perm1, permK). 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)