proposition: Lemma insub_wordcdK n c : c \is a code -> size c <= n.+1 -> [seq (i : nat) | i : 'I_n <- pmap insub (wordcd c)] = wordcd c.
proof: Proof. move=> /wordcd_ltn/allP Hall Hsz. rewrite pmap_filter; last by move=> j /=; rewrite insubK. rewrite (eq_in_filter (a2 := xpredT)); first by rewrite filter_predT. move=> j /= /Hall /= Hj. have {}Hj : j < n by case: (size c) Hj Hsz => [| sz]//=; apply: leq_trans. by rewrite insubT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr