proposition: Lemma leq_dsum_alpha_2l_l l n : S_[l] n + S_[l] n.+1 <= (S_[l.*2] n).*2 + l.
proof: Proof. have H := concaveEk (concave_dsum_alphaL_l n) (leq_addr l l). rewrite addnK addnn -{1}mul2n -{3}[l]mul1n -mulnDl in H. apply: leq_trans (leq_add H (leqnn _)). by rewrite -addnA leq_add2l dsum_alpha3l. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)