proposition: Lemma better_k_bound n k (Hank : (a k <= n < a k.+1)%N) : (k <= trunc_log 2 (trunc_log 2 n) + 2)%N.
proof: Proof. case: k Hank => [| k] //; case: k => [| k Hank]; last exact: k_bound. by rewrite addn2. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis