proposition: Lemma size_std_rec n s : size (std_rec n s) = n.
proof: Proof. Proof using. elim: n s => [// | n IHn] s /=. by rewrite size_cat /= addnS -size_cat cat_take_drop IHn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp