proposition: Lemma is_code_straighten w : rev (straighten w) \is a code.
proof: Proof. Proof using. rewrite /straighten; elim/last_ind: w => [| w wn IHw /=]. rewrite {2}/rev /=. have -> : [:: 0, 0 & nseq n0 0] = nseq n.+1 0 by []. apply/is_codeP => i; rewrite size_rev size_nseq ltnS => Hi. rewrite nth_rev size_nseq ?ltnS //. by rewrite nth_nseq if_same. rewrite rev_rcons => /=. apply (inscodeP IHw). by rewrite size_straighten ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr