proposition: Lemma sorted_iter3 (p : nat) q (s : seq bool) i : i < `2^ p -> `2^ q < size s <= `2^ q.+1 -> p <= q -> let l1 := iter3 (`2^ q) (`2^ p) 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)] -> sorted <=%O (eotake p i l1).
proof: Proof. move=> iLp /andP[qLsl slL2q] pLq s1 [Hl Hr Hw]. apply: sorted_eotake => //. apply: sorted_iter3_aux => //. apply: leq_trans (leq_addr _ _). by rewrite ltnS (leq_trans (ltnW (ltn_ne2n _)) (ltnW qLsl)). split => //. apply/andP; split => //. apply: leq_trans (leq_addl _ _). apply: leq_trans (_ : size (eotake p.+1 i s) <= _). by rewrite -size_noFT leq_addr. rewrite -subSS. by apply: leq_size_eotake_e2n. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort