proposition: Lemma rfd_funP (p : {perm T}) (u : T') : let p1 := if p x == x then p else 1 in p1 (val u) != x.
proof: Proof. case: (p x =P x) => /= [pxx | _]; last by rewrite perm1 (valP u). by rewrite -[x in _ != x]pxx (inj_eq perm_inj); apply: (valP u). 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)