proposition: Lemma sum_alpha_leq n i : i <= n -> \sum_(j < n) alpha j <= (a * \sum_(j < (n - i)) alpha j) + \sum_(j < i) b ^ j.
proof: Proof. have bL1 := bL1. move=> iLn. rewrite -!(big_mkord xpredT) big_distrr /=. suff aux : forall u v w n n0 n1 : nat, u = v + w -> (v != 0) * alpha n <= a * alpha n0 -> (w != 0) * alpha n <= b ^ n1 -> \sum_(n <= i0 < n + u) alpha i0 <= \sum_(n0 <= i < n0 + v) a * alpha i + \sum_(n1 <= i0 < n1 + w) b ^ i0. rewrite -{1}[n]add0n -{1}[n - i]add0n -{2}[i]add0n. apply: aux => //. - by rewrite subnK. - by rewrite !muln1; apply: leq_trans aL1; case: eqP. by rewrite muln1; case: eqP. elim => {i iLn}[[] [] // i j k _ _| u IH [|v] [|w] // i j k uvw aM1 aM2]. - by rewrite !addn0 big_geq. - rewrite big_ltn; last by rewrite addnS leq_addr. rewrite [X in _ <= _ + X]big_ltn; last by rewrite addnS leq_addr. rewrite addnCA. apply: leq_add; first by rewrite mul1n in aM2. rewrite -!addSnnS. apply: IH => //; first by case: uvw. case: (w) => // w1 //. rewrite !mul1n in aM2 |- *. suff /leq_trans-> : alpha i.+1 <= a * alpha i => //. by rewrite expnS; apply: leq_mul => //; apply: ltnW. by apply: alpha_leq_double. - rewrite big_ltn; last by rewrite addnS leq_addr. rewrite [X in _ <= X + _]big_ltn; last by rewrite addnS leq_addr. rewrite -addnA. apply: leq_add; first by rewrite mul1n in aM1. rewrite -!addSnnS. apply: IH => //; first by case: uvw. case: (v) => // v1 //. rewrite !mul1n in aM1 |- *. apply: isAB_leq_alphaSn; first by apply/isAB_amul/isAB_alpha. apply: leq_ltn_trans aM1 _. by rewrite ltn_mul2l ltnW // alpha_ltn. have aM3 : alpha i.+1 <= a * alpha j.+1. rewrite !mul1n in aM1. apply: isAB_leq_alphaSn; first by apply/isAB_amul/isAB_alpha. apply: leq_ltn_trans aM1 _. by rewrite ltn_mul2l ltnW // alpha_ltn. case: (leqP (a * alpha j) (b ^ k)) => [|bLaa]. - rewrite leq_eqVlt => /orP[/eqP aaEb |aaLb]. have : a %| b ^ k by rewrite -aaEb dvdn_mulr. move/gcdn_idPl. have /eqP-> := coprimeXr k aCb. by case: a aL1 => // [] []. - rewrite big_ltn; last by rewrite addnS leq_addr. rewrite [X in _ <= X + _]big_ltn; last by rewrite addnS leq_addr. rewrite -addnA. apply: leq_add; first by rewrite mul1n in aM1. rewrite -2!addSnnS. apply: IH => //; first by case: uvw. case: (v) => // v1 //. by rewrite !mul1n. rewrite !mul1n in aM1, aM2 |- *. apply: isAB_leq_alphaSn (isAB_bexp _) _. by apply: leq_ltn_trans aaLb. rewrite big_ltn; last by rewrite addnS leq_addr. rewrite [X in _ <= _ + X]big_ltn; last by rewrite addnS leq_addr. rewrite addnCA. apply: leq_add; first by rewrite mul1n in aM2. rewrite -addSnnS -(addSnnS k). apply: IH => //; first by move: uvw; rewrite addnS => [[]]. rewrite !mul1n in aM1, aM2 |- *. apply: isAB_leq_alphaSn. by apply: isAB_amul; apply: isAB_alpha. by apply: leq_ltn_trans bLaa. case: (w) => // w1. rewrite !mul1n in aM1, aM2 |- *. apply: isAB_leq_alphaSn (isAB_bexp _) _. apply: leq_ltn_trans aM2 _. by rewrite ltn_exp2l. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)