proposition: Lemma size_iter3 p q (s : seq A) : 0 < q -> size (iter3 p q s) = size s.
proof: Proof. by move=> q_gt; apply/perm_size/perm_iter3. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort