proposition: Lemma is_code_rcons c i : i <= size c -> c \is a code -> rcons c i \is a code.
proof: Proof. move=> Hi /is_codeP Hcode; apply/is_codeP => j. rewrite size_rcons ltnS leq_eqVlt => /orP[/eqP ->| Hj]; rewrite nth_rcons. - by rewrite ltnn eq_refl. - by rewrite Hj; apply Hcode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr