proposition: Lemma std_transp d (T : inhOrderType d) (u v : seq T) a b (U V : seq nat) A B : (a < b)%O -> size u = size U -> std (u ++ [:: a; b] ++ v) = (U ++ [:: A; B] ++ V) -> std (u ++ [:: b; a] ++ v) = (U ++ [:: B; A] ++ V).
proof: Proof. move=> Hab Hsz /eqP/stdP[Hstd Hinv]. apply/eqP/stdP; constructor. + apply: (perm_std Hstd). rewrite perm_cat2l perm_cat2r -[[:: B; A]]cat1s -[[:: A; B]]cat1s. by apply/permPl; exact: perm_catC. + apply: eq_inv_transp => //=. move: Hinv => /eq_invP[_ Hinv]. move/(_ (size u) (size u).+1) : Hinv. set Hyp := (X in (X -> _ ) -> _) => Hinv. have {Hyp}/Hinv : Hyp. by rewrite /Hyp leqnSn /= size_cat /= -addn1 addSnnS leq_add2l. rewrite {3}Hsz !nth_sizeu !{2}Hsz !nth_sizeu1. rewrite (ltW Hab) lt_def => <-; rewrite andbT. move: Hstd => /std_uniq; rewrite cat_uniq => /and3P[_ _ /= /and3P[]]. by rewrite eq_sym inE negb_or => /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp