proposition: Lemma alpha_min_exp3 m k : α m + minn (3 ^ k) (α m) <= α (m + k.+1).
proof: Proof. case: (leqP (α m).*2 (α (m + k.+1))) => [/(leq_trans _)-> //|amkLam]. by rewrite -addnn leq_add2l geq_minr. apply: leq_trans (leq_add (leqnn _) (geq_minl _ _)) _. move: m amkLam => n; rewrite [_ + 3 ^ _]addnC. set m := n + k.+1. have : k + n < m by rewrite /m addnS addnC. move: m => m. elim: k m n => [m n | k IH m n nkLm aL2a]. by rewrite add0n add1n => nLm _; apply: alpha_mono. pose l := [seq (α i) | i <- iota n (m - n).+1 & 3 %| (α i)]. have Il i : i \in l -> exists j, i = 3 * α j. case/mapP => j; rewrite mem_filter => /andP[ajD3 _] ->. have [[i1 [|j1]] /= ajE]: isAB 2 3 (α j) by apply: isAB_alpha. by move: ajD3; rewrite ajE muln1 Euclid_dvdX //. have [k1 ak1E] : {k : nat | α k = 2 ^ i1 * 3 ^ j1} by apply: alpha_surjective. by exists k1; rewrite ak1E ajE expnS mulnCA. have nLm : n <= m by rewrite (leq_trans _ nkLm) // -addSn leq_addl. have iS : k.+3 <= size (iota n (m - n).+1). by rewrite size_iota ltnS leq_subRL // addnC addSn. have kLsl : k.+2 <= size l. rewrite size_map size_filter -ltnS -[X in _ < X]add1n. move: iS; rewrite -(count_predC (fun i => 3 %| (α i))) -/l => iS. apply: leq_trans iS _; rewrite addnC leq_add2r. move: aL2a; rewrite -{1}(subnK nLm) addnC. move: (m - n) => u. elim: u {k IH Il l nLm nkLm}n => [n _ /=|k IH n H]; first by case: negb. have /IH : α (n.+1 + k) < (α n.+1).*2. by rewrite addSnnS (leq_trans H) // leq_double ltnW // alpha_mono. rewrite (iotaS _ _.+1) count_cons. case: ltngtP => // [|H1 _]. by case: count => //=; case: (~~ _). have /hasP[i iH1 iH2] : has (predC (fun i => 3 %| α i)) (iota n.+1 k.+1). by rewrite has_count H1. move: iH1; rewrite mem_iota => /andP[nLi iLn]. rewrite H1; case: (boolP (predC _ _)) => //= iH3. have [[i1 [|j1]] /= aiE] : isAB 2 3 (α i) by apply: isAB_alpha. have [[i2 [|j2]] /= anE] : isAB 2 3 (α n) by apply: isAB_alpha. rewrite !muln1 in aiE anE. have : α n < α i by apply: alpha_mono. rewrite aiE anE ltn_exp2l // => i2Li1. have : (α i) < (α n).*2. apply: leq_trans H; rewrite ltnS -addSnnS //. move: iLn;rewrite addnS ltnS; case: ltngtP => // [iLS _|<-//]. by apply/ltnW/alpha_mono. by rewrite aiE anE -mul2n -expnS ltn_exp2l // ltnS leqNgt i2Li1. by case/negP : iH3; rewrite anE expnS mulnCA dvdn_mulr. by case/negP : iH2; rewrite aiE expnS mulnCA dvdn_mulr. pose n1 := head 0 l. pose m1 := last 0 l. have lS : sorted ltn l. rewrite sorted_map. apply: sorted_filter. by move=> a b c H1 H2; apply: ltn_trans H2. move: (_ - _).+1 => u; elim: u (n) => //= k1 IH1 n0. by case: (k1) (IH1 n0.+1) => //= k2 -; rewrite alpha_mono. have uS : uniq l by move: lS; rewrite ltn_sorted_uniq_leq; case/andP. have n1Il : n1 \in l. by rewrite /n1; case: (l) kLsl => [|a l1]; rewrite /= ?inE ?eqxx. case: (Il _ n1Il) => n2 n2E. have m1Il : m1 \in l. by rewrite /m1; case: (l) kLsl => [|a l1]; rewrite //= mem_last. case: (Il _ m1Il) => m2 m2E. have n1Lm1 : n1 < m1. rewrite /n1 /m1; case: (l) kLsl lS => [|a [|b l1 _]] //= /andP[]. elim: l1 a b => //= c l1 IH1 a b aLb /andP[bLc pH]. by apply: ltn_trans aLb (IH1 _ _ _ _). have n2Lm2 : n2 < m2. move: n1Lm1; rewrite n2E m2E ltn_mul2l /=. case: (ltngtP n2 m2) => // [m2Ln2|->]; last by rewrite ltnn. by rewrite ltnNge ltnW // alpha_mono. pose l1 := [seq 3 * α i | i <- iota n2 (m2 - n2).+1]. have l1size : size l1 = (m2 - n2).+1 by rewrite size_map size_iota. have H : {subset l <= l1}. move=> i iIl; case: (Il _ iIl) => j jE. apply/mapP; exists j; rewrite // mem_iota addnS addnC subnK //; last first. by rewrite ltnW. rewrite ltnS; apply/andP; split. have: n1 <= i. rewrite /n1; case: (l) kLsl iIl lS => //= a l2 _. rewrite inE => /orP[/eqP->//|]. elim: l2 a => //= b l2 IH1 a. rewrite inE => /orP[/eqP->//|bIl2] /andP[aLb pH]; first by apply: ltnW. apply: leq_trans (ltnW aLb) _. by apply: IH1. rewrite n2E jE leq_mul2l /=; case: (ltngtP n2 j) => // jLn2. by rewrite leqNgt alpha_mono. have: i <= m1. rewrite /m1; case: (l) kLsl iIl lS => //= a l2 _. elim: l2 a (i) => /= [a i1|b l2 IH1 a i1]; first by rewrite inE => /eqP->. rewrite inE => /orP[/eqP->//|bIl2] /andP[aLb pH]. apply: leq_trans (ltnW aLb) (IH1 _ _ _ _) => //. by rewrite inE eqxx. by apply: IH1. rewrite m2E jE leq_mul2l /=; case: (ltngtP m2 j) => // jLn2. by rewrite leqNgt alpha_mono. have kn2Lm2 : k + n2 < m2. rewrite -addSn addnC -leq_subRL; last by apply: ltnW. by rewrite -ltnS -l1size (leq_trans kLsl) // uniq_leq_size. have anLan2 : α n <= 3 * α n2. rewrite -n2E. case/mapP : n1Il => i1. rewrite mem_filter mem_iota => /andP[_ /andP[nLi1 _] ->]. by apply: (increasingE increasing_alpha). have am2Lam : 3 * α m2 <= α m. rewrite -m2E. case/mapP : m1Il => i1. rewrite mem_filter mem_iota => /andP[_ /andP[_ i1Lm] ->]. rewrite addnS ltnS addnC subnK // in i1Lm. by apply: (increasingE increasing_alpha). have am2Lan2 : α m2 < (α n2).*2. rewrite -[_ < _]andTb -(ltn_mul2l 3) -doubleMr. apply: leq_ltn_trans am2Lam _. apply: leq_trans aL2a _. by rewrite leq_double. apply: leq_trans am2Lam. apply: leq_trans (leq_add (leqnn _) anLan2) _. rewrite expnS -mulnDr leq_mul2l /=. by apply: IH kn2Lm2 am2Lan2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)