proposition: Lemma bound_dsum_alphaL l n : S_[l] n <= (S_[1] n).*2.
proof: Proof. rewrite S1E. have [SLl|lLS] := leqP (S1 n).*2 l; first by rewrite lim_dsum_alphaL_l. rewrite -(lim_dsum_alphaL_l (leqnn _)). have [/increasingE H _] := concave_dsum_alphaL_l n. by apply/H/ltnW. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)