proposition: Lemma braidredE u v : braid_reduces u v -> 's_[u] = 's_[v].
proof: Proof. Proof using. by move=> /orP[]; [apply braid_prods|apply prods_reducesE]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr