proposition: Lemma cocode_rec_cat m c s : cocode_rec m c s = (cocode_rec m [::] s ++ c).
proof: Proof. Proof using. elim: m => [| m IHm] in c s * => //=. by rewrite IHm [X in _ = X ++ _]IHm -cat1s catA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr