proposition: Lemma rootn_rec_bound k r n : 0 < k -> r <= n -> (rootn_rec k r n) ^ k <= r < (rootn_rec k r n ).+1 ^ k.
proof: Proof. case: k => // k _. have F : 1 < 2 ^ k.+1 by rewrite -{1}[1](exp1n k.+1) ltn_exp2r. elim: n r => [[] //=|n IH [|[|r]] rLn /=]; rewrite ?(exp0n, exp1n) //. rewrite divn_small //=. have -> : rootn_rec k.+1 0 n = 0 by case: (n). by rewrite exp1n /= exp1n. set x := _ %/ _; set u := rootn_rec _ _ _. have /IH : x <= n. apply: leq_trans (rLn : _ < n). have /mulnK H : 0 < 2 ^ k.+1 by rewrite expn_gt0. rewrite -[r.+1]H leq_div2r //. by rewrite -{1}[r.+1]muln1 ltn_mul2l. rewrite -/u => /andP[uLx xLu]. case: (leqP (u.*2.+1 ^ k.+1 ) r.+2) => ->; rewrite !(andbT, andTb). rewrite -doubleS -muln2 expnMn. rewrite (divn_eq r.+2 (2 ^ k.+1)) -/x. apply: leq_trans (_ : x.+1 * 2 ^ k.+1 <= _). by rewrite mulSn addnC ltn_add2r // ltn_mod ?expn_gt0. by rewrite leq_mul2r // expn_eq0. rewrite -muln2 expnMn (divn_eq r.+2 (2 ^ k.+1)) -/x. apply: leq_trans (leq_addr _ _). by rewrite leq_mul2r // expn_eq0. Qed.
imports: mathcomp(all_ssreflect)