proposition: Lemma rembig_ins_std s pos : rembig (take pos (std s) ++ size s :: drop pos (std s)) = std s.
proof: Proof. Proof using. apply: esym; apply/eqP/rembigP; first by case: (take _ _). have:= allLtn_std_rec s. rewrite -{1}[std s](cat_take_drop pos) allLtn_catE => /andP[]. set ll := take _ _; set lr := drop _ _ => /allLtnW Hll Hlr. by exists ll, (size s), lr; split; first rewrite cat_take_drop. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp