proposition: Lemma sorted_eotake (p : nat) (s : seq bool) i : i < `2^ p -> [/\ 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) + 1] -> sorted <=%O (eotake p i s).
proof: Proof. move=> iL2p [/isorted_boolP[[a1 b1] E1 /isorted_boolP[[a2 b2] E2]]]. rewrite E1 E2 !noE addn1 => a2La1. rewrite -eotcat_take // E1 E2. have := size_etake (eotake p i s). have := size_otake (eotake p i s). rewrite etake_eotake // otake_eotake // E1 E2 uphalf_half => <-. rewrite !size_cat !size_nseq. elim: a1 {E1 E2}a2 a2La1 => [[|a2]//= _ Hs|a1 IH [|a2]]. - rewrite eotcat_nseq //. by apply/isorted_boolP; exists (0, b1 + b2). rewrite add0n in Hs. by rewrite Hs; case: odd; rewrite ?add1n !leqnn ?andbT //=. - case: (a1) => // _; case: (b1); case: (b2) => // b3 b4 Hs. rewrite /= in Hs. rewrite ![_ ++ _]/= eotcat_cons (@eotcat_nseq _ true b4.+1). rewrite isorted_consF. by apply/isorted_boolP; exists (0, (b4.+1 + b3).+1). rewrite add1n add0n addnS in Hs. by case: Hs=> ->; case: odd; rewrite ?add1n !leqnn ?andbT /=. rewrite ![_ ++ _]/= !ltnS => HS1 HS2. rewrite !addSn addnS in HS2. rewrite [_ ++ nseq b2 _]/= eotcat_cons !isorted_consF. apply: IH => //. by case: HS2. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort