proposition: Corollary reduced_braid v w : v \is reduced -> w \is reduced -> ('s_[v] == 's_[w] :> 'S_n.+1) = (v =Br w).
proof: Proof. move=> Hv Hw; apply/idP/idP => [/eqP H | /braid_prods -> //]. apply: (braid_trans (braid_to_canword Hv)). rewrite H braid_sym; exact: braid_to_canword. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr