proposition: Lemma in_alphalS n i : i \in alphal n.+1 -> i != a * alpha n -> i != b * alpha n -> i \in alphal n.
proof: Proof. rewrite /alpha /=. set h := head _ _. rewrite mem_merge mem_cat => /orP[]; last first. by case: alphal => //= c l; rewrite inE orbC => ->. by (do 2 case: (_ \in alphal _); rewrite //= ?inE) => [/eqP->|/eqP->|/orP[/eqP->|/eqP->]]; rewrite eqxx. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)