proposition: Lemma nth_iter1 p s (a : A) j : 0 < p -> nth a (iter1 p s) j = if odd (j %/ p) then if j < size s then max (nth a s (j - p)) (nth a s j) else nth a s j else if j + p < size s then min (nth a s j) (nth a s (j + p)) else nth a s j.
proof: Proof. move=> p_gt0. case: (ltnP j (size s)) => jLs; last first. rewrite !nth_default ?minxx ?if_same ?size_iter1 //. by rewrite (leq_trans _ (leq_addr _ _)). apply: nth_iter1_aux; rewrite ?(addn0, add0n) // => j1. rewrite ltn0 andbF. case: (boolP (odd _)) => [j1pO|]//. rewrite ifN // -leqNgt. by rewrite -divn_gt0; case: (_ %/ _) j1pO. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort