proposition: Lemma leq_sum_beta n l a : \sum_(k < n) a k * β_[n, l] k <= \sum_(k < n) a k * (α_[1] k).*2.
proof: Proof. by apply: leq_sum => i _; rewrite leq_mul2l geq_beta orbT. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)