proposition: Lemma braid_rev u v : u =Br v -> rev u =Br rev v.
proof: Proof. Proof using. move: v; apply gencongr_ind; first exact: braid_refl. move=> a b1 c b2 /braid_ltrans ->{u} Hrule. rewrite !rev_cat -!catA; apply braid_is_congr; apply rule_gencongr. move: Hrule; rewrite /braidrule /= !mem_cat => /orP[]. - move/braid_abaP => [x] [y] [Hxy -> ->]. by rewrite /rev /= eq_refl Hxy /= inE eq_refl. - move/braidCP => [x] [y] [Hxy -> ->]. by rewrite /rev /= orbC Hxy mem_seq1 eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr