proposition: Lemma sorted_iter3_aux k (p : nat) q (s : seq bool) i : i < `2^ p -> q < k + p -> let l1 := iter3_aux k (`2^ p) (`2^ q) s in [/\ sorted <=%O (eotake p.+1 i s), sorted <=%O (eotake p.+1 (`2^ p + i) s) & noF (eotake p.+1 (`2^p + i) s) <= noF (eotake p.+1 i s) <= noF (eotake p.+1 (`2^p + i) s) + `2^ (q - p)] -> [/\ sorted <=%O (eotake p.+1 i l1), sorted <=%O (eotake p.+1 (`2^p + i) l1) & noF (eotake p.+1 (`2^p + i) l1) <= noF (eotake p.+1 i l1) <= noF (eotake p.+1 (`2^p + i) l1) + 1].
proof: Proof. move=> iL2p. elim: k q s => [q s | k IH q s qLp]. rewrite [iter3_aux _ _ _ _]/= => qLp. by have -> : q - p = 0 by lia. rewrite [iter3_aux _ _ _ _]/=. case: leqP => [p2Lq2|q2Lp2]. move=> l1; suff -> : q - p = 0 by []. by apply/eqP; rewrite subn_eq0 -leq_e2n. have q_gt0 : 0 < q by rewrite (leq_ltn_trans (_ : 0 <= p)) -1?ltn_e2n. rewrite e2n_div2 // => l1 Hs. apply: IH; try lia. apply: sorted_iter2 => //. by rewrite -ltn_e2n. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort