proposition: Lemma nth_iter2 p q s (a : A) j : 0 < p -> 0 < q -> p %| q -> ~~ odd (q %/ p) -> nth a (iter2 p q s) j = if odd (j %/ p) then if (j + q < size s + p) then min (nth a s j) (nth a s (j + q - p)) else nth a s j else if (q <= j < size s) then max (nth a s (j - q + p)) (nth a s j) else nth a s j.
proof: Proof. move=> p_gt0 q_gt0 pDq qpE. have pLq : p < q. have : p <= q by rewrite dvdn_leq. by case: ltngtP => // pE; case/negP: qpE; rewrite pE divnn q_gt0. case: (ltnP j (size s)) => jLs; last first. rewrite andbF !nth_default ?(maxxx, minxx) ?if_same ?size_iter2 //. by rewrite -addnBA ?(leq_trans jLs (leq_addr _ _)) // ltnW. rewrite andbT. apply: nth_iter2_aux; rewrite ?(addn0, add0n) // => j1. case: (boolP (odd _)) => [j1pO|j1pE]//. have pLj1 : p <= j1 by rewrite -divn_gt0 //; case: (_ %/ _) j1pO. by rewrite ifN // negb_and; case: leqP pLj1. by rewrite ifN // negb_and; case: leqP. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort