proposition: Lemma alphaL_0 l : α_[l] 0 = minn 2 l.
proof: Proof. rewrite /alphaL /delta /dsum_alphaL /conv /= dsum_alpha_1 dsum_alpha_0. by rewrite muln0 addn0 add0n subn0 muln1. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)