proposition: Lemma size_braid u v : u =Br v -> size u = size v.
proof: Proof. Proof using. by move=> /gencongr_invar /= /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr