proposition: Lemma alpha_surjective m n : {k | alpha k = a ^ m * b ^ n}.
proof: Proof. have bL1 := bL1. pose P p := has (fun i => i %| a ^ m * b ^ n) (alphal p). have F1 : exists n, P n. by exists 0; apply/hasP; exists 1. have F2 : 0 < a ^ m * b ^ n. rewrite muln_gt0 !expn_gt0 ?(ltn_trans _ aLb) (ltn_trans _ aL1) //. have F3 p : P p -> p <= alpha (a ^ m * b ^ n). move=> /hasP[q] qIa. suff F : alpha p <= q. move=> /(dvdn_leq F2) H. rewrite ltnW // (leq_trans (alpha_gtn_n _)) //. by rewrite (leq_trans F) // (leq_trans H) // ltnW // alpha_gtn_n. have /= := sorted_alphal p; rewrite /alpha. case: (alphal _) qIa => //= a1 l. by rewrite inE => /orP[/eqP->//|qIl /(order_path_min leq_trans) /allP/(_ _ qIl)]. exists (ex_maxn F1 F3). case: ex_maxnP => i /hasP[x xIa] Hx Fx. have : ~~ P i.+1 by apply/negP=> /Fx; rewrite ltnn. move/hasPn => FF. have F4 : x = alpha i. by apply/eqP; case: eqP=> // /eqP /(in_alphal xIa) /FF/negP[]. case: (isAB_alpha i) => [] [m1 n1 F5]. have Cabe m2 n2 : coprime (a ^ m2) (b ^ n2). case: m2 => [|m2]; first by rewrite coprime1n. case: n2 => [|n2]; first by rewrite coprimen1. by rewrite coprime_pexpl // coprime_pexpr. move: Hx. rewrite F4 F5 Gauss_dvd //=. rewrite Gauss_dvdl // Gauss_dvdr 1?coprime_sym // . rewrite !dvdn_Pexp2l //. rewrite leq_eqVlt => /andP[/orP[/eqP mEm1|H1 H2]]; last first. case/negP: (FF _ (a_in_alphalS _)). rewrite F5 /= mulnA -expnS. by apply: dvdn_mul; apply: dvdn_exp2l. rewrite leq_eqVlt => /orP[/eqP nEn1 //|H1]; first by rewrite mEm1 nEn1. case/negP: (FF _ (b_in_alphalS _)). rewrite mulnC F5 mEm1 /= -mulnA -expnSr. by apply: dvdn_mul; apply: dvdn_exp2l. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)