proposition: Theorem braid_prods v w : v =Br w -> 's_[v] = 's_[w].
proof: Proof. Proof using. move=> H; apply/esym; move: w H; apply gencongr_ind => // a b1 c b2 <- Hrule. rewrite !big_cat /=; congr (_ * (_ * _)). move: Hrule; rewrite {a c} /braidrule /= mem_cat => /orP[]. - move/braid_abaP => [x] [y] [Hxy -> ->]. do 2 (rewrite 2!big_cons big_seq1 mulgA). by move: Hxy => /orP[] /eqP Hxy; rewrite -Hxy eltr_braid // Hxy. - move/braidCP => [x] [y] [Hxy -> ->]. do 2 (rewrite big_cons big_seq1). move: Hxy => /orP[] Hxy. + by rewrite [RHS]eltr_comm // Hxy /=. + by rewrite [LHS]eltr_comm // Hxy /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr