proposition: Lemma cocode2P s : let c := cocode s in c \is a code /\ s = 's_[wordcd c].
proof: Proof. Proof using. rewrite /cocode; apply perm_on_cocode_recP => //. - by rewrite /= big_nil mulg1. - by rewrite /perm_on; apply/subsetP => k _; rewrite !inE; exact: ltn_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr