proposition: Lemma braidrule_sym (u v : seq 'I_n) : v \in (braidrule u) -> u \in (braidrule v).
proof: Proof. Proof using. rewrite !mem_cat => /orP[] /= Hbr; apply/orP. - left; move: Hbr => /braid_abaP[a] [b] [Hab -> ->]. by rewrite /braid_aba eq_refl orbC Hab inE. - right; move: Hbr => /braidCP[a] [b] [Hab -> ->]. by rewrite /braidC orbC Hab inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr