proposition: Lemma iter2_auxS k n p q i (s : seq A) : iter2_aux k.+1 n p q i (s : seq A) = if i + q < n then iter2_aux k n p q i.+1 (if odd (i %/ p) then s else swap (i + p) (i + q) s) else s.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort