proposition: Lemma std_cutabc d (T : orderType d) (u v : seq T) a b c : exists U V A B C, size u = size U /\ std (u ++ [:: a; b; c] ++ v) = (U ++ [:: A; B; C] ++ V).
proof: Proof. set w1 := u ++ _. have Hsz : size u < size (w1). by rewrite /w1 size_cat /= -{1}[size u]addn0 ltn_add2l. exists (take (size u) (std w1)). exists (drop (size u).+3 (std w1)). exists (nth 0 (std w1) (size u)). exists (nth 0 (std w1) (size u).+1). exists (nth 0 (std w1) (size u).+2). split; first by rewrite size_take size_std Hsz. rewrite -{-2}(cat_take_drop (size u) (std w1)); congr (_ ++ _). rewrite drop_cat !nth_cat !size_take size_std Hsz ltnn. rewrite !ltnNge leqnSn /= (leq_trans (leqnSn _) (leqnSn _)) /=. rewrite (leq_trans (leq_trans (leqnSn _) (leqnSn _)) (leqnSn _)) /=. set dr := drop (size u) (std w1). have : size dr >= 3 by rewrite /dr /w1 size_drop size_std size_cat addnC addnK. case H : dr => [// | A [// | B [// | C d']]] _ /=. rewrite !subSn //=; last exact: (@leq_trans (size u).+1). by rewrite subnn drop0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp