proposition: Lemma head_revcode c0 c : rev (c0 :: c) \is a code -> c0 <= size c.
proof: Proof. Proof using. have H : size c < size (rev (c0 :: c)) by rewrite size_rev /= ltnS. move=> /is_codeP/(_ _ H). by rewrite rev_cons nth_rcons size_rev ltnn eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr