proposition: Corollary cocode_straightenE w : rev (straighten w) = cocode 's_[w].
proof: Proof. Proof using. have:= prods_straighten w; rewrite -{1}(canwordP 's_[w]). rewrite -!(big_map nat_of_ord xpredT) /= canwordE /wcord -map_comp. rewrite [map _ _](_ : _ = wordcd (rev (straighten w))); first last. rewrite -[RHS](map_id) -eq_in_map => i. rewrite /= /wordcd => /flatten_mapP[j]. rewrite mem_rev !mem_iota /= add0n size_rev size_straighten ltnS => Hj. move=> /andP[_]; rewrite subnK => [Hij | ]. by rewrite inordK // (leq_trans Hij Hj). have /is_codeP := is_code_straighten w. by rewrite size_rev size_straighten; apply; rewrite ltnS. apply (prods_wordcd_inj (is_code_straighten _) (cocodeP _)). - by rewrite size_rev size_straighten. - exact: size_cocode. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr