proposition: Lemma cycle_type_tperm x y : x != y -> cycle_type (tperm x y) = hookpartn #|T| 1.
proof: Proof. move=> Neq; set ct := cycle_type _. have /(hookpartnPE 0) -> : nth 0 ct 1 <= 1. rewrite -intpartn_count_leq2E {}/ct /cycle_type /= /setpart_shape. set s := (X in sort geq X); have /permPl/seq.permP -> := perm_sort geq s. rewrite {}/s count_map /= -size_filter. rewrite (perm_size (s2 := [:: [set x; y]])) //; apply uniq_perm => //. by apply: filter_uniq; apply enum_uniq. rewrite porbits_tperm => S; rewrite inE mem_filter /= mem_enum. apply/idP/eqP => [ | ->]; last by rewrite !inE eqxx /= andbT cards2 Neq. rewrite andbC !inE => /andP[/orP[/eqP -> // | /imsetP[z _ ->{S}]]]. by rewrite cards1 ltnn. congr hookpartn. rewrite intpartn_nth0 /ct /cycle_type /= /setpart_shape. set s := (X in sort geq X); have /permPl/(perm_big _) -> /= := perm_sort geq s. rewrite {}/s big_map big_enum /=. suff -> : \max_(i in porbits (tperm x y)) #|i| = 2 by []. rewrite porbits_tperm; apply anti_leq; apply/andP; split. apply/bigmax_leqP => /= S. by rewrite !inE=> /orP[/eqP->// | /imsetP[z _ ->{S}]]; rewrite ?cards1 ?cards2 ?Neq. apply: (bigmax_sup [set x; y]); last by rewrite cards2 Neq. by rewrite !inE eqxx. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(tuple finfun finset path bigop) mathcomp(fingroup perm action) mathcomp(ssralg matrix mxalgebra algC classfun) partition tools sorted permcomp fibered_set cycles