proposition: Lemma iter3_auxS k p q (s : seq A) : iter3_aux k.+1 p q (s : seq A) = if q > p then iter3_aux k p q./2 (iter2 p q s) else s.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort