proposition: Theorem size_canword s : size (canword s) = length s.
proof: Proof. Proof using. by rewrite -(size_map val) canwordE size_wordcd sumn_cocode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr