proposition: Lemma sum_alpha_eq n i : b ^ i <= alpha n < b ^ i.+1 -> \sum_(i0 < n.+1) alpha i0 = (a * \sum_(i0 < (n - i)) alpha i0) + \sum_(i0 < i.+1) b ^ i0.
proof: Proof. have bL1 := bL1. elim: n i => [i|n IH i]. case: i => [_|i]; last by rewrite leqNgt alpha0 (ltn_exp2l 0). by rewrite !big_ord_recr !big_ord0 muln0. rewrite leq_eqVlt => /andP[/orP[/eqP Ha Hb| Ha Hb]]. case: i Ha Hb => [H|i Ha Hb]. have : alpha 0 < alpha n.+1 by apply: alpha_mono. by rewrite [alpha 0]H ltnn. rewrite big_ord_recr [X in _ = _ + X]big_ord_recr /= Ha. rewrite addnA; congr (_ + _). rewrite subSS. apply: IH => //. rewrite Ha alpha_ltn andbT. apply: isAB_geq_alphaSn (isAB_bexp _) _. by rewrite -Ha ltn_exp2l. rewrite subSn; last exact: b_exp_ltn Ha. rewrite big_ord_recr [X in _ = _ * X + _]big_ord_recr. rewrite mulnDr addnAC. congr (_ + _); last first. by apply: alpha_b_eq; rewrite ?Ha. apply: IH. rewrite (isAB_geq_alphaSn (isAB_bexp _)) //. apply: leq_trans Hb. by rewrite ltnS ltnW // alpha_ltn. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)