proposition: Lemma b_exp_leq k n : b ^ k <= alpha n -> k <= n.
proof: Proof. have bL1 := bL1. elim: n k => [k|n IH [|k Hk]//]. by rewrite -[alpha 0]/(b ^ 0) leq_exp2l. apply/IH/(isAB_geq_alphaSn (isAB_bexp _)). by apply: leq_trans Hk; rewrite ltn_exp2l. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)