proposition: Lemma canword_eltr (i : 'I_n) : canword 's_i = [:: i].
proof: Proof. suff /braid_to_canword : [:: i] \is reduced. by rewrite big_seq1 braid_sym => /class_braid1. by apply/reducedP; rewrite big_seq1 length_eltr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr