proposition: Lemma code_ltn_size c : c \is a code -> all (gtn (size c)) c.
proof: Proof. move=> /is_codeP Hcode. apply/allP => /= v /[dup]/(nth_index 0){-1}<-. by rewrite -index_mem => /[dup] Hv /Hcode/leq_ltn_trans; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr