proposition: Theorem prods_straighten w : 's_[wcord (straighten w)] = 's_[w].
proof: Proof. Proof using. move: (straighten_path_npos w) => [p] [Hpath <-]. elim: p w Hpath => [| p0 p IHp] //= w /andP[/braidredE ->{w}]. exact: IHp. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr