proposition: Lemma nth_swap a i j (s : seq A) k : i < j < size s -> nth a (swap i j s) k = (if k == i then min (nth a s i) (nth a s j) else if k == j then max (nth a s i) (nth a s j) else nth a s k).
proof: Proof. case: s => [/andP[]|/= b s /andP[iLj jLs]]; first by case: j. rewrite nth_cat size_take /= (ltn_trans iLj jLs). case: (ltngtP k i) => [kLi|iLk|->]; first 2 last. - rewrite subnn /=; congr min. rewrite -nth0 nth_drop addn0. by apply: set_nth_default; rewrite /= (ltn_trans iLj). rewrite -nth0 nth_drop addn0 nth_behead nth_drop prednK ?subn_gt0 //. by rewrite addnC subnK 1?ltnW //; apply: set_nth_default. - by rewrite ?nth_take // ifN // neq_ltn (ltn_trans kLi). rewrite -[k - i]prednK ?subn_gt0 //=. rewrite nth_cat size_take size_behead size_drop /=. rewrite !prednK ?subn_gt0 // subSn /=; last first. by rewrite -ltnS (leq_trans iLj (ltnW _)). rewrite leq_sub2r // -ltnS prednK ?subn_gt0 //. rewrite -(ltn_add2r i) !subnK //; try by rewrite ltnW. case: (ltngtP k j) => [kLj|jLk|->]; first 2 last. - rewrite subnn /= -!nth0 !(nth_drop, nth_behead) !addn0. rewrite prednK ?subn_gt0 // addnC subnK; last by rewrite ltnW. congr max; apply: set_nth_default => //. by rewrite (leq_trans iLj (ltnW _)). - rewrite nth_take; last first. rewrite -ltnS !prednK ?subn_gt0 //. by rewrite -(ltn_add2r i) !subnK // ltnW. - by rewrite nth_behead nth_drop prednK ?subn_gt0 // addnC subnK // ltnW. rewrite -[_.-1 - _.-1]subSS !prednK ?subn_gt0 //. rewrite subnBA 1?ltnW // subnK 1?ltnW // -[k - j]prednK ?subn_gt0 //=. rewrite !(nth_behead, nth_drop) prednK ?subn_gt0 // -addSn prednK ?subn_gt0 //. by rewrite addnCA addnA subnK 1?ltnW // addnC subnK 1?ltnW. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort