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