proposition: Lemma increasing_dsum_alphaL_l n : increasing (fun l => S_[l] n).
proof: Proof. move=> l; rewrite /increasing /dsum_alphaL /conv. apply: leq_bigmin => i _. by rewrite leq_add2l leq_mul2r leqnSn orbT. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)