proposition: Lemma braid_abaP (u v : seq 'I_n) : reflect (exists a b : 'I_n, [/\ ((a.+1 == b) || (b.+1 == a)), u = [:: a; b; a] & v = [:: b; a; b] ] ) (v \in braid_aba u).
proof: Proof. Proof using. rewrite /braid_aba /=; apply: (iffP idP). - case: u => [//=|u0[//=|u1[//=|u2[]//=]]]. case H : ((u0 == u2) && ((u0.+1 == u1) || (u1.+1 == u0))). + move: H => /andP[/eqP <- Heq]. rewrite mem_seq1 => /eqP ->. by exists u0, u1. + by rewrite in_nil. - by move=> [a] [b] [H -> ->]; rewrite H eq_refl /= inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr