proposition: Corollary canword_path_npos w : { p | path braidred w p /\ last w p = canword 's_[w] }.
proof: Proof. Proof using. by rewrite -canword_straightenE; exact: straighten_path_npos. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr