proposition: Lemma straighten_path_npos w : { p | path braidred w p /\ last w p = wcord (straighten w) }.
proof: Proof. Proof using. rewrite /straighten; elim/last_ind: w => [| w wn]. exists [::]; split; first by []. rewrite [LHS]/=; apply esym; apply/nilP. by rewrite /wcord /nilp size_map size_wordcd sumn_rev /= !add0n; elim: n0. rewrite rev_rcons /= -/(straighten w) -cats1 => [] [prec] [Hpath Hlast]. have : size (straighten w) <= n0.+2 by rewrite size_straighten. move=> /(braidred_inscode_path (is_code_straighten w)) => Hins. have : wn.+1 < size (straighten w) by rewrite size_straighten ltnS. move=> {}/Hins [pins] [Hpathins Hlastins]. exists ([seq v ++ [:: wn] | v <- prec] ++ pins); split => [| {Hpath Hpathins}]. - rewrite cat_path (last_map (fun v => v ++ [:: wn])) Hlast Hpathins andbT. exact: path_braidred_catl. - by rewrite last_cat (last_map (fun v => v ++ [:: wn])) Hlast. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr