proposition: Lemma increasing_alphaL_l n : increasing (fun l => α_[l] n).
proof: Proof. move=> l; rewrite !alphaLE !fmergeE //; last 4 first. - by move=> k; rewrite leq_double; apply/ltnW/alpha_mono. - by move=> k; rewrite leq_mul2l leq_exp2l ?leqnSn ?orbT. - by move=> k; rewrite leq_double; apply/ltnW/alpha_mono. - by move=> k; rewrite leq_mul2l leq_exp2l ?leqnSn ?orbT. apply/bigmax_leqP => i _. apply: leq_trans (_ : minn (α i).*2 (l.+1 * 3 ^ (n - i)) <= _). by rewrite leq_min !geq_min leqnn /= leq_mul2r leqnSn !orbT. by apply: leq_bigmax. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)