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