fact: Fixpoint std_rec n s := if n is n'.+1 then let rec := std_rec n' (rembig s) in let pos := posbig s in take pos rec ++ n' :: drop pos rec else [::].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp