proposition: Lemma size_knuth_jump_rec m k : size (knuth_jump_rec m k ((`2^ k).-1)) = k.
proof: Proof. elim: k => //= k IH. by rewrite -e2Sn uphalfE prednK ?e2n_gt0 // e2Sn addnn doubleK IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort