proposition: Lemma sorted_iknuth_exchange_aux k (p : nat) q (s : seq bool) : 0 < q -> `2^ q < size s <= `2^ q.+1 -> p <= q -> p < k -> let s1 := iknuth_exchange_aux k (`2^ q) (`2^ p) s in (forall i, i < `2^ p -> [/\ sorted <=%O (eotake p.+1 i s) & sorted <=%O (eotake p.+1 (`2^ p + i) s)]) -> sorted <=%O s1.
proof: Proof. move=> g_gt0. elim: k p s => // k IH [|p] s qLs pLq pLk s1 Hs. rewrite {}/s1. case: {IH pLk}k => /= [|_]. - apply: (@sorted_iter3 0 q (iter1 1 s) 0) => //. by rewrite size_iter1. have [|H1 H2]// := Hs 0. by apply: sorted_iter1. apply: (@sorted_iter3 0 q (iter1 1 s) 0) => //. by rewrite size_iter1. have [|H1 H2]// := Hs 0. by apply: sorted_iter1. rewrite /s1 /= -e2Sn e2n_gt0 e2n_div2 //. apply: IH => //. - by rewrite size_iter3 ?e2n_gt0 // size_iter1 ?e2n_gt0. - by rewrite /= // (leq_trans _ pLq). move=> i Hi. split => //. have iL2p : i < `2^ p.+1 by apply: leq_trans Hi _; rewrite leq_e2n. have [Hs1 Hs2] := Hs _ iL2p. apply: sorted_iter3 => //. by rewrite size_iter1 ?e2n_gt0. by apply: sorted_iter1. have iL2p : `2^ p + i < `2^ p.+1 by rewrite ltn_add2l. have [Hs1 Hs2] := Hs _ iL2p. apply: sorted_iter3 => //. by rewrite size_iter1 ?e2n_gt0. by apply: sorted_iter1. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort