proposition: Lemma size_iter1_aux k n p i (s : seq A) : 0 < p -> n = size s -> size (iter1_aux k n p i s) = size s.
proof: Proof. by move=> p_gt0 nE; apply/perm_size/perm_iter1_aux. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort