proposition: Lemma perm_iter3_aux k p q (s : seq A) : 0 < p -> perm_eq (iter3_aux k p q s) s.
proof: Proof. move=> p_gt0. elim: k q s => //= k IH q s. case: leqP => // H. apply: perm_trans. apply: IH. by apply: perm_iter2. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort