proposition: Lemma alphaL_1_2 n : α_[1] (n.+1) <= (α_[1] n).*2.
proof: Proof. rewrite !alphaL1E. case: n => // [] [|[|[|]]] // k. rewrite -(leq_pmul2l (_ : 0 < 3)) //. rewrite -!alphaL1E. apply: leq_trans (alpha_4_3 _) _ => //. by rewrite -mul2n mulnA leq_mul2r orbT. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)