proposition: Lemma wcordE c : rev c \is a code -> size c <= n.+1 -> wcord c = pmap insub (wordcd (rev c)).
proof: Proof. Proof using. rewrite /wcord => Hcode; have:= Hcode => /wordcd_ltn/allP. rewrite size_rev => Hall Hsz. apply (inj_map (@val_inj _ _ _)) => /=. rewrite insub_wordcdK //; last by rewrite size_rev. rewrite -map_comp -[RHS]map_id -eq_in_map => j /Hall /= Hj. rewrite inordK //. by case: (size c) Hj Hsz => [| sz] //=; exact: leq_trans. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr