proposition: Lemma b_exp_ltn k n : b ^ k < alpha n -> k < n.
proof: Proof. case: n => [|n H]; first by rewrite ltnNge expn_gt0 (leq_trans _ bL1). by rewrite ltnS; apply/b_exp_leq/(isAB_geq_alphaSn (isAB_bexp _)). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)