proposition: Lemma std_drop_std u v : std (drop (size u) (std (u ++ v))) = std v.
proof: Proof. apply/eqP/std_eq_invP. rewrite -{2}(drop_size_cat v (erefl (size u))). apply (eq_inv_catr (u1 := take (size u) (std (u ++ v))) (u2 := take (size u) (u ++ v)) ). - by rewrite !cat_take_drop; apply eq_inv_sym; apply: eq_inv_std. - by rewrite !size_take size_std. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp