proposition: Lemma isAB_geq_alphaSn i v : isAB v -> v < alpha i.+1 -> v <= alpha i.
proof: Proof. move => isAB; have := @isAB_leq_alphaSn i _ isAB. by do 2 case: leqP => // _. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)