proposition: Lemma std_take_std u v : std (take (size u) (std (u ++ v))) = std u.
proof: Proof. apply/eqP/std_eq_invP. rewrite -{3}(take_size_cat v (erefl (size u))). apply (eq_inv_catl (v1 := drop (size u) (std (u ++ v))) (v2 := drop (size u) (u ++ v)) ). - by rewrite !cat_take_drop; apply eq_inv_sym; exact: eq_inv_std. - by rewrite !size_take size_std. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp