proposition: Lemma reduced_sprod_code c : c \is a code -> size c <= n.+1 -> pmap insub (wordcd c) \is reduced.
proof: Proof. Proof using. move=> Hcode Hsz; apply/reducedP. have:= Hsz => /(length_permcd Hcode) Hlength. rewrite -(big_map nat_of_ord xpredT) /=. by rewrite -(size_map val) /= insub_wordcdK // Hlength size_wordcd. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr