proposition: Lemma porbits_mul_tperm s x y : let t := tperm x y in #|porbits (t * s)| + (x \notin porbit s y).*2 = #|porbits s| + (x != y).
proof: Proof. pose xf a b u := seq.find (pred2 a b) (traject u (u a) #|porbit u a|). have xf_size a b u: xf a b u <= #|porbit u a|. by rewrite (leq_trans (find_size _ _)) ?size_traject. have lt_xf a b u n : n < xf a b u -> ~~ pred2 a b ((u ^+ n.+1) a). move=> lt_n; apply: contraFN (before_find (u a) lt_n). by rewrite permX iterSr nth_traject // (leq_trans lt_n). pose t a b u := tperm a b * u. have tC a b u : t a b u = t b a u by rewrite /t tpermC. have tK a b: involutive (t a b) by move=> u; apply: tpermKg. have tXC a b u n: n <= xf a b u -> (t a b u ^+ n.+1) b = (u ^+ n.+1) a. elim: n => [|n IHn] lt_n_f; first by rewrite permM tpermR. rewrite !(expgSr _ n.+1) !permM {}IHn 1?ltnW //; congr (u _). by case/lt_xf/norP: lt_n_f => ne_a ne_b; rewrite tpermD // eq_sym. have eq_xf a b u: pred2 a b ((u ^+ (xf a b u).+1) a). have ua_a: a \in porbit u (u a) by rewrite porbit_sym (mem_porbit _ 1). have has_f: has (pred2 a b) (traject u (u a) #|porbit u (u a)|). by apply/hasP; exists a; rewrite /= ?eqxx -?porbit_traject. have:= nth_find (u a) has_f; rewrite has_find size_traject in has_f. rewrite -eq_porbit_mem in ua_a. by rewrite nth_traject // -iterSr -permX -(eqP ua_a). have xfC a b u: xf b a (t a b u) = xf a b u. without loss lt_a: a b u / xf b a (t a b u) < xf a b u. move=> IHab; set m := xf b a _; set n := xf a b u. by case: (ltngtP m n) => // ltx; [apply: IHab | rewrite -[m]IHab tC tK]. by move/lt_xf: (lt_a); rewrite -(tXC a b) 1?ltnW //= orbC [_ || _]eq_xf. pose ts := t x y s; rewrite /= -[_ * s]/ts. pose dp u := #|porbits u :\ porbit u y :\ porbit u x|. rewrite !(addnC #|_|) (cardsD1 (porbit ts y)) imset_f ?inE //. rewrite (cardsD1 (porbit ts x)) inE imset_f ?inE //= -/(dp ts) {}/ts. rewrite (cardsD1 (porbit s y)) (cardsD1 (porbit s x)) !(imset_f, inE) //. rewrite -/(dp s) !addnA !eq_porbit_mem andbT; congr (_ + _); last first. wlog suffices: s / dp s <= dp (t x y s). by move=> IHs; apply/eqP; rewrite eqn_leq -{2}(tK x y s) !IHs. apply/subset_leq_card/subsetP=> {dp} C. rewrite !inE andbA andbC !(eq_sym C) => /and3P[/imsetP[z _ ->{C}]]. rewrite 2!eq_porbit_mem => sxz syz. suffices ts_z: porbit (t x y s) z = porbit s z. by rewrite -ts_z !eq_porbit_mem {1 2}ts_z sxz syz imset_f ?inE. suffices exp_id n: ((t x y s) ^+ n) z = (s ^+ n) z. apply/porbit_setP => u; apply/idP/idP=> /porbitP[i ->]. by rewrite /aperm exp_id mem_porbit. by rewrite /aperm -exp_id mem_porbit. elim: n => // n IHn; rewrite !expgSr !permM {}IHn tpermD //. by apply: contraNneq sxz => ->; apply: mem_porbit. by apply: contraNneq syz => ->; apply: mem_porbit. case: eqP {dp} => [<- | ne_xy]; first by rewrite /t tperm1 mul1g porbit_id. suff ->: (x \in porbit (t x y s) y) = (x \notin porbit s y) by case: (x \in _). without loss xf_x: s x y ne_xy / (s ^+ (xf x y s).+1) x = x. move=> IHs; have ne_yx := nesym ne_xy; have:= eq_xf x y s; set n := xf x y s. case/pred2P=> [|snx]; first exact: IHs. by rewrite -[x \in _]negbK ![x \in _]porbit_sym -{}IHs ?xfC ?tXC // tC tK. rewrite -{1}xf_x -(tXC _ _ _ _ (leqnn _)) mem_porbit; symmetry. rewrite -eq_porbit_mem eq_sym eq_porbit_mem porbit_traject. apply/trajectP=> [[n _ snx]]. have: looping s x (xf x y s).+1 by rewrite /looping -permX xf_x inE eqxx. move/loopingP/(_ n); rewrite -{n}snx. case/trajectP=> [[_|i]]; first exact: nesym; rewrite ltnS -permX => lt_i def_y. by move/lt_xf: lt_i; rewrite def_y /= eqxx orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)