proposition: Lemma braidred_size_decr w p : path braidred w p -> size w >= size (last w p).
proof: Proof. elim: p w => [| p0 p IHp] //= w /andP[HBr /IHp/leq_trans]; apply. move: HBr => /orP[ /size_braid -> // |]. move/reducesP => [x] [i] [y] [-> ->]. by rewrite !size_cat [size [:: i; i] + _]addnC addnA; exact: leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr