fact: Definition braid_reduces (u v : seq 'I_n) := (u =Br v) || (reduces u v).
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr