proposition: Lemma increasing_alphaL l : increasing α_[l].
proof: Proof. apply: increasing_ext; first by move=> i; apply/sym_equal/alphaLE. apply: increasing_fmerge. by move=> n; rewrite leq_double; apply/ltnW/alpha_mono. by move=> n; rewrite leq_mul2l leq_exp2l ?leqnSn ?orbT. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)