proposition: Lemma isAB_alphal n i : i \in alphal n -> isAB i.
proof: Proof. elim: n i => /= [i|n IH i]; rewrite ?mem_merge ?inE. case/or3P => /eqP->; first by exists (0, 0). by apply: (isAB_aexp 1). by apply: (isAB_bexp 1). have F : i \in behead (alphal n) -> exists m, i = a ^ m.1 * b ^ m.2. by move=> U; apply: IH (mem_behead _). have [[m1 m2 Hm]] : exists m, head 1 (alphal n) = a ^ m.1 * b ^ m.2. case: (alphal n) IH => /= [_|c l F1]; first by exists (0, 0). by apply: F1; rewrite inE eqxx. (do 2 case: (_ \in alphal _)); rewrite /= ?inE. - by apply: F. rewrite /=. - case/orP=> [/eqP->|/F//]; exists (m1, m2.+1). by rewrite /= Hm mulnCA expnS. - case/orP=> [/eqP->|/F//]; exists (m1.+1, m2). by rewrite Hm expnS !mulnA. case/or3P=> [/eqP->|/eqP->|//]. by exists (m1.+1, m2); rewrite Hm expnS !mulnA. by exists (m1, m2.+1); rewrite /= Hm mulnCA expnS. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)