proposition: Lemma geq_beta n l k : β_[n, l] k <= (α_[1] k).*2.
proof: Proof. rewrite /beta; case: (_ < _) => //=. by case: (_ == _) => //=; apply: bound_alphaL. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)