proposition: Lemma isAB_leq_alphaSn i v : isAB v -> alpha i < v -> alpha i.+1 <= v.
proof: Proof. case=> [] [m1 m2 ->]. case: (alpha_surjective m1 m2) => j <- iLj. case: (leqP i.+1 j) => [|H]. by rewrite leq_eqVlt => /orP[/eqP->//|/alpha_mono/ltnW]. move: H iLj; rewrite [alpha _ < _]ltnNge. rewrite ltnS leq_eqVlt => /orP[/eqP->//|/alpha_mono/ltnW->//]. by rewrite leqnn. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)