proposition: Lemma leperm_factorP s t : reflect (exists2 w : seq 'I_n0, w \is reduced & exists2 l : nat, t = 's_[w] & s = 's_[take l w]) (s <=R t).
proof: Proof. apply (iffP (lepermP s t)) => /= [[u] ->{t} Hlen | [w] Hred [l] Ht Hs]. - exists (canword s ++ canword u). apply/reducedP; rewrite size_cat !size_canword -Hlen. by rewrite big_cat /= !canwordP. exists (length s). + by rewrite big_cat /= !canwordP. + by rewrite take_size_cat ?size_canword // canwordP. - exists (\prod_(i <- drop l w) 's_i). + by rewrite Ht Hs -big_cat /= cat_take_drop. + rewrite {}Hs {}Ht (reducedP Hred). rewrite -{1}(cat_take_drop l w) in Hred. rewrite (reducedP (reduced_catl Hred)) (reducedP (reduced_catr Hred)). by rewrite -size_cat cat_take_drop. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype