proposition: Lemma is_codeP c : reflect (forall i, i < size c -> nth 0 c i <= i) (c \is a code).
proof: Proof. rewrite /unfold_in; apply (iffP idP) => [/allP Hcode // i Hi | Hcode]. - by apply Hcode; rewrite mem_iota /= add0n. - by apply/allP => i; rewrite mem_iota add0n /=; exact: Hcode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr