proposition: Lemma class_braid1 (i : 'I_n) u : u =Br [:: i] -> u = [:: i].
proof: Proof. rewrite braid_sym. move: u; apply: gencongr_ind => //= a b1 c b2 /(congr1 size) /= Hsize. by rewrite mem_cat => /orP[/braid_abaP | /braidCP] [x [y]] [_ Hb1 _]; exfalso; move: Hsize; rewrite Hb1 !size_cat /= !addnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr