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