proposition: Lemma wordcd_ltn c : c \is a code -> all (gtn (size c).-1) (wordcd c).
proof: Proof. move=> /is_codeP Hcode. apply/allP => i /flatten_mapP[ j]; rewrite mem_iota /= add0n => Hc. rewrite mem_rev mem_iota subnK; last exact: Hcode. move=> /andP[_ /leq_trans]; apply. by case: (size c) Hc. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr