proposition: Theorem braid_to_canword w : w \is reduced -> w =Br canword 's_[w].
proof: Proof. move/reducedP; rewrite -size_canword braid_sym. case: (braidred_to_canword w) => p [Hpath <-]. elim: p w Hpath => [| p0 p IHp] //= w /andP[]. rewrite {1}/braidred => /orP[] HBr. - move/IHp; rewrite (size_braid HBr) => /[apply] /braid_ltrans ->. by rewrite braid_sym. - move=> {IHp} /braidred_size_decr Hsz Heq; exfalso. move: Hsz; rewrite {}Heq. move/reducesP: HBr => [x] [i] [y] [-> ->]. rewrite !size_cat [size [:: i; i] + _]addnC addnA /=. by rewrite leqNgt addnS ltnS addn1 leqnSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr