proposition: Lemma k_bound n k (Hank : a k <= n < a k.+1) (le2k : k >= 2) : k <= trunc_log 2 (trunc_log 2 n) + 2.
proof: Proof. case/andP: Hank => lean lena. case: k lean lena le2k => // k lean lena le2k. case: k lean lena le2k => // k lean lena le2k. rewrite -addn1 -addn1 -addnA addn1. rewrite leq_add // . exact: hanson_5. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial