proposition: Lemma rfd_odd (p : {perm T}) : p x = x -> rfd p = p :> bool.
proof: Proof. have rfd1: rfd 1 = 1. by apply/permP => u; apply: val_inj; rewrite permE /= if_same !perm1. have [n] := ubnP #|[set x | p x != x]|; elim: n p => // n IHn p le_p_n px_x. have [p_id | [x1 Hx1]] := set_0Vmem [set x | p x != x]. suffices ->: p = 1 by rewrite rfd1 !odd_perm1. by apply/permP => z; apply: contraFeq (in_set0 z); rewrite perm1 -p_id inE. have nx1x: x1 != x by apply: contraTneq Hx1 => ->; rewrite inE px_x eqxx. have npxx1: p x != x1 by apply: contraNneq nx1x => <-; rewrite px_x. have npx1x: p x1 != x by rewrite -px_x (inj_eq perm_inj). pose p1 := p * tperm x1 (p x1). have fix_p1 y: p y = y -> p1 y = y. by move=> pyy; rewrite permM; have [<-|/perm_inj<-|] := tpermP; rewrite ?pyy. have p1x_x: p1 x = x by apply: fix_p1. have{le_p_n} lt_p1_n: #|[set x | p1 x != x]| < n. move: le_p_n; rewrite ltnS (cardsD1 x1) Hx1; apply/leq_trans/subset_leq_card. rewrite subsetD1 inE permM tpermR eqxx andbT. by apply/subsetP=> y /[!inE]; apply: contraNneq=> /fix_p1->. transitivity (p1 (+) true); last first. by rewrite odd_permM odd_tperm -Hx1 inE eq_sym addbK. have ->: p = p1 * tperm x1 (p x1) by rewrite -tpermV mulgK. rewrite morphM; last 2 first; first by rewrite 2!inE; apply/astab1P. by rewrite 2!inE; apply/astab1P; rewrite -[RHS]p1x_x permM px_x. rewrite odd_permM IHn //=; congr (_ (+) _). pose x2 : T' := Sub x1 nx1x; pose px2 : T' := Sub (p x1) npx1x. suffices ->: rfd (tperm x1 (p x1)) = tperm x2 px2. by rewrite odd_tperm eq_sym; rewrite inE in Hx1. apply/permP => z; apply/val_eqP; rewrite permE /= tpermD // eqxx. by rewrite !permE /= -!val_eqE /= !(fun_if sval) /=. 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)