proposition: Corollary length_eq1 s : length s = 1%N -> exists i : 'I_n0, s = 's_i.
proof: Proof. rewrite -size_canword -{2}(canwordP s). case: (canword s) => [|i[|j]] // _. by exists i; rewrite big_seq1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr