proposition: Lemma inscodeP c (i : 'I_n) : rev c \is a code -> i.+1 < size c -> rev (inscode c i) \is a code.
proof: Proof. Proof using. elim: c i => [//= | c0 c IHc] i /= => Hcode. have:= Hcode; rewrite rev_cons => /is_code_rconsK Hcd. move/(_ _ Hcd): IHc => Hrec. have /head_revcode := Hcode => Hc0. move/is_codeP : Hcode; rewrite size_rev /= => Hcode. rewrite !ltnS => Hisz. case: ltnP => Hi. rewrite rev_cons. move/(_ _ (inord_predS Hi Hisz)) : Hrec => /= /is_code_rcons; apply. by rewrite size_rev size_inscode. case: eqP => [Hi1 | /eqP Hi1]. rewrite rev_cons; apply: (is_code_rcons _ Hcd). rewrite size_rev; apply (leq_trans (leq_pred _)). have := Hcode (size c) (ltnSn (size c)). by rewrite rev_cons nth_rcons size_rev ltnn eq_refl. have {Hi1}Hi : i < size c - c0 by rewrite ltn_neqAle Hi Hi1. case: eqP => [Hi1 | /eqP Hi1]. rewrite rev_cons; apply: (is_code_rcons _ Hcd). by rewrite size_rev -subn_gt0 -Hi1. have {Hi1}Hi : i.+1 < size c - c0 by rewrite ltn_neqAle Hi Hi1. rewrite rev_cons. have /Hrec : i.+1 < size c by apply (leq_trans Hi); exact: leq_subr. move/is_code_rcons; apply. by rewrite size_rev size_inscode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr