proposition: Lemma bound_alphaL l n : α_[l] n <= (α_[1] n).*2.
proof: Proof. rewrite alphaL1E. have [SLl|lLS] := leqP (S1 n.+1).*2 l. rewrite /alphaL /delta !lim_dsum_alphaL_l //. by rewrite -delta_S1 doubleB. by apply: leq_trans SLl; case: convex_2S1. rewrite -delta_S1 /delta doubleB. rewrite -(lim_dsum_alphaL_l (leqnn _)). rewrite -[(S1 n).*2](@lim_dsum_alphaL_l (S1 n.+1).*2). rewrite -[_ - _]/(α_[_] _). by apply: increasingE (increasing_alphaL_l n) _; apply: ltnW. by case: convex_2S1. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)