proposition: Lemma nth_iter2_aux k n p q i s s1 (a : A) : 0 < p -> 0 < q -> p %| q -> ~~ odd (q %/ 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) && (j + q < n + p) then min (nth a s j) (nth a s (j + q - p)) else nth a s j else if (q <= j < i + q) then max (nth a s (j - q + p)) (nth a s j) else nth a s j) -> (forall j, j < n -> nth a (iter2_aux k n p q i s1) j = if odd (j %/ p) then if (j + q < n + p) then min (nth a s j) (nth a s (j + q - p)) else nth a s j else if (q <= j) 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 pDqE nEl nEl1. have pLq : p < q. have : p <= q by rewrite dvdn_leq. by case: ltngtP => // pE; case/negP: pDqE; rewrite pE divnn q_gt0. 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 (leq_trans jLn _) (leq_addr q i)) // andbT. by rewrite (leq_trans (leq_trans jLn _) (leq_addr p i)) // andbT. case: (ltnP (i + q)) => [iqLn|nLiq]; last first. have := Hc j. have [jpO|jpE]/= := boolP (odd _). case: (ltnP (j + q)); rewrite !(andbT, andbF) // => jqLnp. case: (ltnP j); rewrite // leqNgt. by rewrite -(ltn_add2r q) (leq_trans jqLnp) // addnAC leq_add2r. by rewrite (leq_trans jLn _) // andbT. have iqB : i + p < i + q < n by rewrite ltn_add2l pLq iqLn. rewrite IH //. - by case: odd; rewrite // size_swap // -nEl1. - by rewrite -addSnnS. move=> j1. case: (boolP (odd _)) => [ipO|ipE]/=. have iqO : odd ((i + q) %/ p). case/dvdnP: pDq pDqE => r ->. by rewrite mulnK // divnDMl // oddD => /negPf->; rewrite addbF. case: (boolP (odd _)) => [j1pO|j1pE]/=. have j1Dip : j1 != i + p. rewrite -[odd _]negbK in j1pO. apply: contra j1pO => /eqP->. by rewrite -[X in _ + X]mul1n divnDMl // addn1 /= negbK. by rewrite Hc j1pO addSn /= ltnS [j1 <= _]leq_eqVlt (negPf j1Dip). rewrite Hc (negPf j1pE) /=. rewrite ltnS [j1 <= _]leq_eqVlt; case: eqP =>> //= j1Ei. by case/negP: j1pE; rewrite j1Ei. rewrite nth_swap -?nEl1 //. have ipO : odd ((i + p) %/ p). by rewrite -[X in _ + X]mul1n divnDMl // addn1 /=. have iqE : ~~ odd ((i + q) %/ p). case/dvdnP: pDq pDqE => r ->. by rewrite mulnK // divnDMl // oddD => /negPf->; rewrite addbF. case: eqP => [->|/eqP j1Di]. rewrite -[X in _ + X]mul1n divnDMl // addn1 /= ipE mul1n. rewrite leqnn. rewrite addnAC ltn_add2r iqLn /=. by rewrite !Hc (negPf iqE) ipO !ltnn !andbF /= addnK. case: eqP => [->|/eqP j1Dip]. rewrite (negPf iqE) leq_addl leqnn /= addnK. by rewrite !Hc (negPf iqE) ipO !ltnn !leq_addl. case: (boolP (odd _)) => [j1pO|j1pE]. by rewrite Hc j1pO addSn ltnS [j1 <= _]leq_eqVlt (negPf j1Di). by rewrite Hc (negPf j1pE) ltnS [j1 <= _]leq_eqVlt (negPf j1Dip). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort