proposition: Theorem braidred_to_canword w : { p | path braidred w p /\ last w p = canword 's_[w] }.
proof: Proof. case: (n =P 0) => Hn. subst n; case: w => [| [w0 Hw0] w] //=. by rewrite big_nil canword1; exists [::]. move: Hn; case H : {1}(n) => _ //=; subst n. exact: canword_path_npos. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr