proposition: Lemma perm_swap (s : seq A) i j : i < j < size s -> perm_eq (swap i j s) s.
proof: Proof. case: s => //= a s /andP[iLj jLs]. rewrite -[X in perm_eq _ X](cat_take_drop i). rewrite perm_cat2l. have := size_drop i (a :: s). rewrite /= -[_ - _]prednK; last first. by rewrite subn_gt0 (ltn_trans iLj). case: drop => //= a1 l1. rewrite prednK; last by rewrite subn_gt0 (ltn_trans iLj). move=> sl1E. rewrite -[X in perm_eq _ (_ :: X)](cat_take_drop (j - i).-1). move: (sl1E) => sl1E1. have jBiL : j - i < (size s).+1 - i. rewrite -(ltn_add2r i) !subnK //; last by apply: ltnW. by apply: (leq_trans (ltnW iLj) (ltnW _)). rewrite -[l1](cat_take_drop (j - i).-1) size_cat size_take ifT in sl1E; last by rewrite -ltnS sl1E1 prednK ?subn_gt0. case: drop sl1E => [|b l2 _] /=. rewrite addn0 prednK ?subn_gt0 // => jBiE. by rewrite jBiE ltnn in jBiL. case: (ltP a1 b) => _ //. rewrite -!seq.cat_cons -!cat_rcons perm_cat2r /=. set l4 := take _ _. have <- := perm_rcons b (rcons l4 a1). rewrite perm_sym. have <- := perm_rcons a1 (rcons l4 b). rewrite -[X in perm_eq X]cats0 !cat_rcons. rewrite -[X in perm_eq _ X]cats0 !cat_rcons. rewrite perm_cat2l. by have <- := perm_rcons b [::a1]. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort