proposition: Theorem reduceP u : u \isn't reduced -> exists v w, u =Br v /\ reduces v w.
proof: Proof. rewrite unfold_in => Hnred. have {Hnred} : length ((\prod_(i <- u) 's_ i) : 'S_n.+1) < size u. by rewrite ltn_neqAle Hnred length_prods. rewrite -size_canword. case: (braidred_to_canword u) => p [Hpath <-]. elim: p u Hpath => [| p0 p IHp] u //=; first by rewrite ltnn. rewrite {1}/braidred => /andP[/orP[] HBr]. - move/IHp; rewrite (size_braid HBr) => /[apply]. move=> [v] [w] [/(braid_trans HBr) {HBr} Hred]. by exists v, w. - by exists u, p0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr