proposition: Lemma alpha_b_eq n i : b ^ i < alpha n.+1 < b ^ i.+1 -> alpha n.+1 = a * alpha (n - i).
proof: Proof. have bL1 := bL1. move=> /andP[beLa aLbe]. have iLm : i <= n. apply/b_exp_leq/isAB_geq_alphaSn => //. by exists (0, i); rewrite mul1n. have [[[|x] y] Hxy] : isAB (alpha n.+1) by apply: isAB_alpha. move: beLa aLbe; rewrite Hxy. rewrite mul1n !(ltn_exp2l _ _ bL1) ltnS. by case: leqP. case: (alpha_surjective x y) => k Hk. pose la := [seq alpha (j : 'I_n.+2) | j <- enum 'I_n.+2]. pose lb := [seq b ^ (j : 'I_ i.+1) | j <- enum 'I_i.+1]. pose lc := [seq a * alpha (j : 'I_(n - i)) | j <- enum 'I_(n- i)]. have Ula : uniq la. rewrite map_inj_uniq; first by apply: enum_uniq. move=> k1 k2 H. case: (leqP k1 k2)=> [|/alpha_mono]; last by rewrite H ltnn. by rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono]; rewrite H ltnn. have Sla : size la = n.+2 by rewrite size_map size_enum_ord. pose la1:= [seq x <- la | a %| x]. pose la2 := [seq x <- la | ~~ (a %| x)]. pose lk := [seq a * alpha (j : 'I_k.+1) | j <- enum 'I_k.+1]. have Slk : size lk = k.+1 by rewrite size_map size_enum_ord. have lkEla1 : lk =i la1. move=> u; rewrite mem_filter. apply/mapP/idP. case => z Hz ->; rewrite dvdn_mulr //=. have [[x1 y1] Hx1y1] : isAB (alpha z) by apply: isAB_alpha. case: (alpha_surjective x1.+1 y1) => t Ht. suff H1t : t < n.+2. apply/mapP; exists (Ordinal H1t); first by rewrite mem_enum. by rewrite Ht expnS -mulnA -Hx1y1. case: leqP => // /alpha_mono. rewrite ltnNge Hxy Ht /= !expnS -!mulnA -Hx1y1 -Hk. rewrite (leq_pmul2l (ltnW aL1)). have : z < k.+1 by []. by rewrite ltnS leq_eqVlt => /orP[/eqP->|/alpha_mono/ltnW->]; rewrite // leqnn. rewrite andbC => /andP[/mapP[v Hv ->] Ha]. have [[[|x1] y1] Hx1y1] : isAB (alpha v) by apply: isAB_alpha. move: Ha; rewrite Hx1y1 mul1n /= => /gcdn_idPl. have /eqP-> : coprime a (b ^ y1) by rewrite coprimeXr. by move=> H; move: aL1; rewrite H ltnn. case: (alpha_surjective x1 y1) => j1 Hj1. suff H1j1 : j1 < k.+1. exists (Ordinal H1j1); first by rewrite mem_enum. by rewrite Hx1y1 expnS -mulnA Hj1. case: leqP => // /alpha_mono. rewrite -(ltn_pmul2l (ltnW aL1)) Hk Hj1 !mulnA -!expnS -Hxy -Hx1y1. rewrite ltnNge isAB_geq_alphaSn //; first by apply: isAB_alpha. by apply: alpha_mono. have lbEla2 : lb =i la2. move=> u; apply/idP/idP; last first. rewrite mem_filter andbC => /andP[/mapP[v Hx ->]]. have /alpha_mono : v < n.+2 by []. case: (isAB_alpha v) => [] [[|u1] v1]->/=; last first. by rewrite expnS -mulnA dvdn_mulr. rewrite mul1n => H _. have /(ltn_pexp2l (ltnW bL1)) v1Li : b ^ v1 < b ^ i.+1. apply: leq_ltn_trans aLbe. by apply: isAB_geq_alphaSn (isAB_bexp _) _. by apply/mapP; exists (Ordinal v1Li); rewrite // mem_enum. move=> /mapP[u1 _ ->]. rewrite mem_filter; apply/andP; split. apply/negP=> /gcdn_idPl. have /eqP-> : coprime a (b ^ u1) by rewrite coprimeXr. by move=> H; move: aL1; rewrite H ltnn. case: (alpha_surjective 0 u1) => j1; rewrite mul1n => Hj1. suff j1Ln : j1 < n.+2. by apply/mapP; exists (Ordinal j1Ln); rewrite ?mem_enum. case: leqP => // /alpha_mono; rewrite ltnNge => /negP[]. apply: leq_trans (ltnW beLa). by rewrite Hj1 leq_exp2l // -ltnS. rewrite Hxy expnS -mulnA -Hk. congr (_ * alpha _). rewrite -subSS -subSS -Sla (_ : size la = size la1 + size la2); last first. by rewrite !size_filter count_predC. have : uniq la1. apply: filter_uniq. rewrite map_inj_uniq; first by apply: enum_uniq. move=> k1 k2 H. case: (leqP k1 k2)=> [|/alpha_mono]; last by rewrite H ltnn. by rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono]; rewrite H ltnn. rewrite (uniq_size_uniq _ lkEla1) => [/eqP->|]; last first. rewrite map_inj_uniq; first by apply: enum_uniq. move=> k1 k2 H. case: (leqP k1 k2)=> [|/alpha_mono]; last first. by rewrite -(ltn_pmul2l (ltnW aL1)) H ltnn. rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono]. by rewrite -(ltn_pmul2l (ltnW aL1)) H ltnn. rewrite Slk. have : uniq la2. apply: filter_uniq. rewrite map_inj_uniq; first by apply: enum_uniq. move=> k1 k2 H. case: (leqP k1 k2)=> [|/alpha_mono]; last by rewrite H ltnn. by rewrite leq_eqVlt => /orP[/val_eqP//|/alpha_mono]; rewrite H ltnn. rewrite (uniq_size_uniq _ lbEla2) => [/eqP->|]; last first. rewrite map_inj_uniq; first by apply: enum_uniq. by move=> k1 k2 /eqP; rewrite eqn_exp2l => // /val_eqP. rewrite size_map size_enum_ord. by rewrite subSS addnK. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)