proposition: Lemma canwordE s : [seq (i : nat) | i : 'I_n0 <- canword s] = wordcd (cocode s).
proof: Proof. Proof using. by apply (insub_wordcdK (cocodeP _)); rewrite size_cocode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr