proposition: Lemma alpha_mono m n : m < n -> alpha m < alpha n.
proof: Proof. elim: n => // n IH. have F := alpha_ltn n. by rewrite ltnS leq_eqVlt => /orP[/eqP->| /IH /ltn_trans-> //]. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)