proposition: Lemma isAB_alpha n : isAB (alpha n).
proof: Proof. rewrite /alpha. case: (alphal n) (alphal_neq_nil n) (@isAB_alphal n (head 1 (alphal n))) => //= c l _. by apply; rewrite inE eqxx. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)