proposition: Lemma wcord_cons c i : wcord (i :: c) = wcord c ++ map inord (rev (iota (size c - i) i)).
proof: Proof. Proof using. rewrite /wcord /wordcd -map_cat; congr (map _ _). rewrite size_rev [size (_ :: _)]/= -(addn1 (size c)) iotaD. rewrite !map_cat !flatten_cat /= cats0 !add0n !rev_cons. rewrite nth_rcons size_rev ltnn eq_refl. congr ((flatten _) ++ _); apply eq_in_map => j. by rewrite mem_iota /= add0n nth_rcons size_rev => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr