proposition: Lemma sorted_knuth_jump_rec m (t : (m + m).-tuple bool) k : sorted <=%O (tetake t) -> sorted <=%O (totake t) -> noF (totake t) <= noF (tetake t) <= noF (totake t) + `2^ k -> sorted <=%O (nfun (knuth_jump_rec (m + m) k (`2^ k).-1) t).
proof: Proof. move=> teS toS /andP[noL noI]. set t1 := nfun _ _. pose i := noF (tetake t) - noF (totake t). suff [te1S to1S noFE] : [/\ sorted <=%O (tetake t1), sorted <=%O (totake t1) & noF (tetake t1) = noF (totake t1) + odd i]. apply: sorted_tetake_totake => //. by rewrite noFE; case: odd; rewrite !(addn1, addn0) leqnn leqnSn. have : i <= `2^ k by rewrite leq_subLR. elim: k t teS toS @i @t1 {noI} noL => [|k IH] t teS toS i; rewrite [nfun _ _]/= => t1 nt2Lnt1 iL2k. rewrite teS toS /i. move: iL2k; rewrite leq_subLR addn1. case: ltngtP nt2Lnt1 => // [|->]; last by rewrite subnn addn0. case: (ltngtP (noF (totake _)).+1) => // <-. by rewrite subSn // subnn addn1. move: @t1; set cf := cfun _ _ => t1. have k2O : odd (`2^ k.+1).-1. by rewrite -[odd _]negbK -oddS prednK ?e2n_gt0 // e2Sn addnn odd_double. have uhE : (uphalf (`2^ k.+1).-1).*2 = `2^ k.+1. by rewrite uphalfE prednK ?e2n_gt0 // e2Sn addnn doubleK -addnn. have iLuh : i <= (uphalf (`2^ k.+1).-1).*2 by rewrite uhE. have [] := sorted_odd_jump k2O iLuh teS toS. by rewrite addnC subnK. rewrite doubleB uhE -/cf => te1S to1S nteE. move: @t1; rewrite -e2Sn. have -> : (uphalf (`2^ k.+1).-1).-1 = (`2^ k).-1. by rewrite uphalfE prednK ?e2n_gt0 // e2Sn addnn doubleK. have -> : odd i = odd (noF (tetake cf) - noF (totake cf)). rewrite nteE addnC addnK oddB. by rewrite e2Sn addnn -doubleB odd_double addbC. by rewrite leq_subLR -addnn leq_add2r. apply: IH => //; first by rewrite nteE leq_addr. rewrite nteE addnC addnK leq_subLR. have [iLk|kLi] := leqP i (`2^ k); first by apply: leq_trans (leq_addl _ _). rewrite e2Sn -addnn subnDA subnK. by rewrite -addnBA ?leq_addr // ltnW. rewrite leq_subRL //. by rewrite !addnn leq_double // ltnW. by apply: (leq_trans (ltnW _) (leq_addr _ _)). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort