proposition: Lemma perm_iter2 p q (s : seq A) : 0 < p -> p < q -> perm_eq (iter2 p q s) s.
proof: Proof. by move=> p_gt0 pLq; apply: perm_iter2_aux. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort