proposition: Lemma in_alphal n i : i \in alphal n -> i != alpha n -> i \in alphal n.+1.
proof: Proof. have := alpha_gt0 n. rewrite /alpha /= mem_merge mem_cat orbC. case: (alphal n) => //= c l cP. by rewrite inE => /orP[/eqP->|->//]; rewrite eqxx. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)