proposition: Lemma leq_log3_alpha n : log3 (α n) < n.+1.
proof: Proof. rewrite -(ltn_exp2l _ _ (_ : 1 < 3)) //. apply: leq_ltn_trans (leq_log3 _) _; first by apply: alpha_gt0. by apply: alpha_exp_bound. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)