proposition: Lemma nth_iter1_aux k n p i s s1 (a : A) : 0 < p -> n = size s -> n = size s1 -> n <= k + i -> (forall j, nth a s1 j = if odd (j %/ p) then if (j < i + p) then max (nth a s (j - p)) (nth a s j) else nth a s j else if (j + p < n) && (j < i) then min (nth a s j) (nth a s (j + p)) else nth a s j) -> (forall j, j < n -> nth a (iter1_aux k n p i s1) j = if odd (j %/ p) then max (nth a s (j - p)) (nth a s j) else if j + p < n then min (nth a s j) (nth a s (j + p)) else nth a s j).
proof: Proof. move=> p_gt0 nEl nEl1. elim: k i s1 nEl1 => [i s1 nEl1 nLi /= Hc j jLn| /= k IH i s1 nEl1 nLi Hc j jLn /=]. have := Hc j. rewrite (leq_trans jLn nLi) andbT. suff -> : j < i + p by []. by rewrite (leq_trans (leq_trans jLn nLi) (leq_addr _ _)). case: (ltnP (i + p)) => [ipLn|nLip]; last first. have := Hc j. have [jpO|jpE] := boolP (odd _). by rewrite ifT // (leq_trans jLn). case: (ltnP (j + p)) => [jpLn|nLjp]//=. by rewrite -(ltn_add2r p) (leq_trans jpLn). have ipB : i < i + p < n. by rewrite -ltn_subLR // subnn p_gt0. rewrite IH //. - by case: odd; rewrite // size_swap // -nEl1. - by rewrite -addSnnS. move=> j1. case: (boolP (odd _)) => [ipO|ipE]. case: (boolP (odd _)) => [jpO|jpE]. have j1Dip : j1 != i + p. rewrite -[odd _]negbK in jpO. apply: contra jpO => /eqP->. by rewrite -[X in _ + X]mul1n divnDMl // addn1 /= negbK. by rewrite Hc jpO addSn ltnS [j1 <= _]leq_eqVlt (negPf j1Dip). rewrite Hc (negPf jpE) /=. rewrite ltnS [j1 <= _]leq_eqVlt; case: eqP =>> //= j1Ei. by case/negP: jpE; rewrite j1Ei. rewrite nth_swap -?nEl1 //. case: eqP => [->|/eqP j1Di]. rewrite (negPf ipE) ltnS ipLn leqnn //=. rewrite !Hc (negPf ipE) ipLn !ltnn /=. by rewrite -[X in _ + X]mul1n divnDMl // addn1 /= ipE mul1n. case: eqP => [->|/eqP j1Dip]. rewrite leqnn. rewrite -[X in _ + X]mul1n divnDMl // addn1 /= ipE mul1n addnK. rewrite !Hc (negPf ipE) ipLn !ltnn /=. by rewrite -[X in _ + X]mul1n divnDMl // addn1 /= ipE mul1n. case: (boolP (odd _)) => [j1pO|j1pE]. by rewrite Hc j1pO addSn ltnS [j1 <= _]leq_eqVlt (negPf j1Dip). by rewrite Hc (negPf j1pE) ltnS [j1 <= _]leq_eqVlt (negPf j1Di). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort