proposition: Lemma perm_iter2_aux k n p q i (s : seq A) : 0 < p -> p < q -> n = size s -> perm_eq (iter2_aux k n p q i s) s.
proof: Proof. move=> p_gt0 pLq. elim: k i s => //= k1 IH i s nE. case: ltnP => // ipLn. have ipB : i + p < i + q < n by rewrite ltn_add2l pLq. apply: perm_trans (IH _ _ _) _. by case: odd => //=; rewrite size_swap // -nE. by case: odd => //; apply: perm_swap; rewrite -nE. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort