proposition: Lemma dsum_alphaLE l n : S_[l] n = \sum_(i < n) α_[l] i.
proof: Proof. elim: n => [|n IH]. by rewrite /dsum_alphaL /conv /= dsum_alpha_0 muln0 big_ord0. by rewrite dsum_alphaL_S IH big_ord_recr. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)