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