proposition: Lemma leperm_succ s t : s <R t -> exists2 i : 'I_n0, (s <R s * 's_i) & (s * 's_i <=R t).
proof: Proof. move=> /andP[sNt /leperm_factorP[w wred [l Ht Hs]]]. have : l < size w. by move: sNt; apply contraR; rewrite Ht Hs -leqNgt => /take_oversize ->. case Hw : w => // [w0 wtl]; rewrite -{}Hw {wtl} => Hl. have lens : length s = l. have := size_take l w; rewrite Hl => <-. rewrite Hs; apply/reducedP. by move: wred; rewrite -{1}(cat_take_drop l w) => /reduced_catl. have eqs1 : s * 's_(nth w0 w l) = \prod_(i <- take l.+1 w) 's_i. by rewrite (take_nth w0 Hl) -cats1 big_cat /= big_seq1 -Hs. have lens1 : length (s * 's_(nth w0 w l)) = l.+1. rewrite -(size_takel Hl) eqs1; apply/reducedP. by move: wred; rewrite -{1}(cat_take_drop l.+1 w) => /reduced_catl. exists (nth w0 w l). - rewrite lt_neqAle; apply/andP; split. + by apply/negP=> /eqP/(congr1 length)/eqP; rewrite lens lens1; elim l. + apply/lepermP; exists ('s_(nth w0 w l)) => //. by rewrite lens lens1 length_eltr addn1. - apply/lepermP; exists (\prod_(i <- drop l.+1 w) 's_i). + by rewrite eqs1 -big_cat cat_take_drop /= -Ht. + have:= wred; rewrite -{1}(cat_take_drop l.+1 w)=>/reduced_catr/reducedP->. rewrite lens1 size_drop subnKC // Ht. exact/reducedP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype