proposition: Lemma sorted_iter2 (p : nat) q (s : seq bool) i : i < `2^ p -> p < q -> let s1 := iter2 (`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 s1), sorted <=%O (eotake p.+1 (`2^p + i) s1) & noF (eotake p.+1 (`2^p + i) s1) <= noF (eotake p.+1 i s1) <= noF (eotake p.+1 (`2^p + i) s1) + `2^ (q.-1 - p)].
proof: Proof. move=> iL2p pLq s1. have q_gt0 : 0 < q by apply: leq_ltn_trans pLq. have p2Lq2 : `2^ p < `2^ q by rewrite ltn_e2n. have p2Dq2 : `2^ p %| `2^ q by rewrite dvdn_e2n ltnW. set s2 := eotake _ _ _; set s3 := eotake _ _ _. pose d : nat := (size s2 != size s3). move=> [] /isorted_boolP[[a1 b1] s2E] /isorted_boolP[[a2 b2] s3E]. pose sl := eotake p i s. pose xi := a1 - a2. pose j := xi - `2^(q - p.+1). have ss2E : size s2 = uphalf (size sl) by rewrite -size_etake etake_eotake. have ss3E : size s3 = (size sl)./2 by rewrite -size_otake otake_eotake. have dE : d = odd (size sl). rewrite /d ss2E ss3E uphalf_half; case odd; rewrite /= ?eqxx ?add1n //. by case: ltngtP (leqnn (size sl)./2.+1). rewrite uphalf_half -dE s2E size_cat !size_nseq in ss2E. rewrite s3E size_cat !size_nseq in ss3E. have a1b1E : a1 + b1 = a2 + b2 + d by rewrite ss2E addnC ss3E. rewrite s3E s2E !noE => a1B. pose s4 := nseq (a1 - j) false ++ nseq (b1 + j) true. have s4S : size s4 = size (eotake p.+1 i s1). rewrite size_cat !size_nseq. rewrite (eq_size_eotake _ _ (size_iter2 s (e2n_gt0 _) _)) //. rewrite -/s2 s2E size_cat !size_nseq. lia. pose s5 := nseq (a2 + j) false ++ nseq (b2 - j) true. have s5S : size s5 = size (eotake p.+1 (`2^ p + i) s1). rewrite size_cat !size_nseq. rewrite (eq_size_eotake _ _ (size_iter2 s (e2n_gt0 _) _)) //. rewrite -/s3 s3E size_cat !size_nseq. rewrite -subSS subSn // e2Sn in a1B. lia. have xiLpq : xi <= `2^ (q - p) by lia. have <- : s4 = eotake p.+1 i s1. apply: (@eq_from_nth _ true) => // k kLs. rewrite !nth_cat !nth_nseq size_nseq if_same. rewrite nth_eotake /s1 nth_iter2 ?e2n_gt0 //; last first. rewrite -[q]prednK // e2Sn addnn -muln2. rewrite -divn_mulAC ?muln2 ?odd_double // dvdn_e2n //. by rewrite -ltnS prednK. rewrite -nth_eotake -/s2 !modn_small; last first. by rewrite (leq_trans iL2p) // leq_addr. rewrite s2E !nth_cat !nth_nseq !size_nseq if_same. rewrite [X in (i + X * _) %/ _]e2Sn addnn -doubleMl doubleMr. rewrite [_ * _.*2]mulnC divnDMl ?e2n_gt0 // oddD odd_double. rewrite divn_small //=. have := kLs; rewrite s4S => /gtn_size_eotake. have ss : size s1 = size s. by apply: size_iter2 => //; apply: e2n_gt0. rewrite ss => ->; last first. by rewrite // ?(leq_trans _ (leq_addr _ _)) //. rewrite andbT. case: ltnP => [kLa1j|a1jLk]. rewrite (leq_trans kLa1j (leq_subr _ _)). case: leqP => // q2Lipk. have qp2L1k : `2^ (q -p) <= 1 + k.*2. have : `2^ q <= `2^ p + (`2^ p + `2^ p) * k by apply: leq_trans q2Lipk _; rewrite leq_add2r ltnW. rewrite -[in X in X <= _](subnK (ltnW pLq)) e2nD. rewrite addnn -doubleMl doubleMr. rewrite -[X in _ <= X + _]mul1n [`2^ p * _]mulnC -mulnDl leq_mul2r. by case: e2n (e2n_gt0 p). have qp2Lk : `2^ (q - p) <= k.*2. have := half_leq qp2L1k. rewrite e2n_div2 ?subn_gt0 // halfD /= odd_double /= -leq_double. by rewrite -addnn -e2Sn doubleK prednK // subn_gt0. rewrite -addnBA; last first. rewrite -e2Sn -(subnK pLq) e2nD mulnC leq_mul2l. case: e2n (e2n_gt0 p.+1) => //= _ _. by rewrite subnS -e2n_div2 ?subn_gt0 // leq_half_double. rewrite [i + _ + _]addnAC [i + `2^ _]addnC. rewrite -e2Sn -(subnK pLq) [_ - _ + _]addnC e2nD -mulnBr. rewrite -[_ + i](modn_small (_ : _ < `2^ p.+1)); last by rewrite ltn_add2l. rewrite -nth_eotake -/s3 s3E nth_cat !nth_nseq /= size_nseq. case: leqP => //. have : (`2^ (q -p.+1)).*2 = `2^ (q -p). by rewrite -addnn -e2Sn -subSn. lia. case: (leqP (`2^ q)) => [q2Lipk|ipkLq2]. have qp2L1k : `2^ (q -p) <= 1 + k.*2. have : `2^ q <= `2^ p + (`2^ p + `2^ p) * k by apply: leq_trans q2Lipk _; rewrite leq_add2r ltnW. rewrite -[in X in X <= _](subnK (ltnW pLq)) e2nD. rewrite addnn -doubleMl doubleMr. rewrite -[X in _ <= X + _]mul1n [`2^ p * _]mulnC -mulnDl leq_mul2r. by case: e2n (e2n_gt0 p). have qp2Lk : `2^ (q - p) <= k.*2. have := half_leq qp2L1k. rewrite e2n_div2 ?subn_gt0 // halfD /= odd_double /= -leq_double. by rewrite -addnn -e2Sn doubleK prednK // subn_gt0. rewrite -addnBA; last first. rewrite -e2Sn -(subnK pLq) e2nD mulnC leq_mul2l. case: e2n (e2n_gt0 p.+1) => //= _ _. by rewrite -leq_double -addnn -e2Sn -subSn. rewrite [i + _ + _]addnAC [i + `2^ _]addnC. rewrite -e2Sn -(subnK pLq) [_ - _ + _]addnC e2nD -mulnBr. rewrite -[_ + i](modn_small (_ : _ < `2^ p.+1)); last by rewrite ltn_add2l. rewrite -nth_eotake -/s3 s3E nth_cat !nth_nseq /= size_nseq. case: leqP => // k2pqLa2; first by rewrite if_same maxTb. case: leqP => //. lia. case: leqP => //. have : (`2^ (q -p) * `2^ p) = `2^ q by rewrite -e2nD subnK // ltnW. have : (`2^ (q -p.+1)).*2 = `2^ (q -p) by rewrite -addnn -e2Sn -subSn. move=> {ss kLs xiLpq s5S s4S a1B a1b1E ss2E ss3E dE s3E s2E p2Dq2}//. by nia. have <- : s5 = eotake p.+1 (`2^ p + i) s1. apply: (@eq_from_nth _ true) => // k kLs. rewrite !nth_cat !nth_nseq size_nseq if_same. rewrite nth_eotake /s1 nth_iter2 ?e2n_gt0 //; last first. rewrite -[q]prednK // e2Sn addnn -muln2. rewrite -divn_mulAC ?muln2 ?odd_double // dvdn_e2n //. by rewrite -ltnS prednK. rewrite -nth_eotake -/s2 !modn_small; last first. by rewrite ltn_add2l. rewrite -/s3. rewrite s3E !nth_cat !nth_nseq !size_nseq if_same. rewrite [X in (_ + i + X * _) %/ _]e2Sn addnn -doubleMl doubleMr. rewrite [_ * _.*2]mulnC divnDMl ?e2n_gt0 // oddD odd_double. rewrite -[X in (X + i) %/ _]mul1n [X in X %/ _]addnC divnDMl ?e2n_gt0 //. rewrite addn1 /= divn_small //=. rewrite -!addnA [`2^ p + (_ + _)]addnC !addnA addnK ltn_add2r. case: (ltnP k a2) => [kLa2|a2Lk]. rewrite (leq_trans kLa2 (leq_addr _ _)). by rewrite minFb if_same. rewrite minTb. case: leqP => [a2jLk|kLa2j]. case: leqP => // q2Lipk. rewrite -[i](modn_small (_ : _ < `2^ p.+1)); last first. by rewrite e2Sn; lia. rewrite -e2Sn -(subnK pLq) e2nD -addnA [_ * k]mulnC -mulnDl mulnC. rewrite -nth_eotake. rewrite -/s2 s2E nth_cat !nth_nseq /= size_nseq if_same. by case: leqP => //; lia. rewrite ifT; last first. have kqpLa1 : k + `2^ (q - p.+1) < a1 by lia. have iL2p1 : i < `2^ p.+1 by rewrite (leq_trans iL2p (leq_addr _ _)). have kqpLss2 : k + `2^ (q - p.+1) < size s2. by rewrite s2E size_cat !size_nseq; lia. rewrite -e2Sn. have <- : (`2^ (q -p.+1) * `2^ p.+1) = `2^ q by rewrite -e2nD subnK // ltnW. rewrite [_ * `2^ p.+1]mulnC -addnA -mulnDr. by apply: gtn_size_eotake iL2p1 kqpLss2. rewrite -[i](modn_small (_ : _ < `2^ p.+1)); last first. by rewrite e2Sn; lia. rewrite -e2Sn -(subnK pLq) e2nD -addnA [_ * k]mulnC -mulnDl mulnC. rewrite -nth_eotake. rewrite -/s2 s2E nth_cat !nth_nseq /= size_nseq if_same. by case: leqP => //; lia. split. - by apply/isorted_boolP; exists (a1 - j, b1 + j). - by apply/isorted_boolP; exists (a2 + j, b2 - j). rewrite !noE. have : (`2^ (q.-1 - p)).*2 = `2^ (q -p). by rewrite -addnn -e2Sn -subSn ?prednK; lia. have : (`2^ (q - p.+1)).*2 = `2^ (q -p). rewrite -addnn -e2Sn -subSn ?subSS //. lia. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort