proposition: Lemma length_permcd c : c \is a code -> size c <= n -> length 's_[wordcd c] = sumn c.
proof: Proof. Proof using. rewrite wordcdE => /[dup] Hcode /is_codeP Hcd Hsz. rewrite (sumn_nth_le (n := size c)) // /index_iota subn0. have [n] := ubnPgeq (size c); elim: n => [/= |m IHm] Hm. by rewrite !big_nil length1. rewrite -(addn1 m) iotaD !big_cat /= add0n !big_seq1. rewrite perm_on_prods_length /=; first by rewrite (IHm (ltnW Hm)). - exact: leq_trans Hm Hsz. - by apply Hcd. - rewrite -/(index_iota _ _). apply: (perm_on_prods Hcode (ltnW Hm)). by apply ltnW; exact: leq_trans Hm Hsz. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr