FormalConjecturesForMathlib.NumberTheory.AdditionChain

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Data.List.Sort
public import Mathlib.Order.Lattice.Nat

@[expose] public section

Addition chains

An addition chain for $n$ is a strictly increasing sequence $1 = a_0 < a_1 < \cdots < a_r = n$ in which every entry after the first is the sum of two earlier entries. Its length is $r$, the number of additions, and $\ell(n)$ is the least length over all chains ending at $n$.

additionChainLength is an infimum over List ℕ, so an explicit chain bounds it above (additionChainLength_le) but nothing bounds it below until the search is confined. The confinement here is that an addition step at most doubles, so r steps cannot reach past 2 ^ r (getLast_le_two_pow), giving lt_additionChainLength_of_two_pow_lt.

An addition chain is a strictly increasing sequence $1 = a_0 < a_1 < \cdots < a_r$ in which every entry after the first is the sum of two (not necessarily distinct) earlier entries.

IsAdditionChain c asserts that the list $c$ is such a chain: it starts at $1$, is strictly increasing, and every entry other than $1$ is a sum of two entries of $c$.

def IsAdditionChain (c : List ℕ) : Prop :=
  c.head? = some 1 ∧
  c.Pairwise (· < ·) ∧
  ∀ x ∈ c, x ≠ 1 → ∃ y ∈ c, ∃ z ∈ c, x = y + z

Every quantifier in IsAdditionChain is bounded by the list, so membership is decidable and a concrete chain can be checked by decide.

instance (c : List ℕ) : Decidable (IsAdditionChain c) := byc:List ℕ⊢ Decidable (IsAdditionChain c)
  unfold IsAdditionChainc:List ℕ⊢ Decidable (c.head? = some 1 ∧ List.Pairwise (fun x1 x2 ↦ x1 < x2) c ∧ ∀ x ∈ c, x ≠ 1 → ∃ y ∈ c, ∃ z ∈ c, x = y + z); infer_instanceAll goals completed! 🐙

The length $\ell(n)$ of $n$: the minimal number of addition steps (the number of entries minus one) over all addition chains ending at $n$.

noncomputable def additionChainLength (n : ℕ) : ℕ :=
  sInf { r | ∃ c : List ℕ, IsAdditionChain c ∧ c.getLast? = some n ∧ c.length = r + 1 }

The set of step counts realised by chains ending at n.

def additionChainSteps (n : ℕ) : Set ℕ :=
  { r | ∃ c : List ℕ, IsAdditionChain c ∧ c.getLast? = some n ∧ c.length = r + 1 }

theorem additionChainLength_eq_sInf (n : ℕ) :
    additionChainLength n = sInf (additionChainSteps n) := rfl

Exhibiting a chain bounds ℓ above.

theorem additionChainLength_le {n r : ℕ} (c : List ℕ) (hc : IsAdditionChain c)
    (hlast : c.getLast? = some n) (hlen : c.length = r + 1) : additionChainLength n ≤ r :=
  Nat.sInf_le ⟨c, hc, hlast, hlen⟩

theorem additionChainSteps_nonempty {n r : ℕ} (c : List ℕ) (hc : IsAdditionChain c)
    (hlast : c.getLast? = some n) (hlen : c.length = r + 1) : (additionChainSteps n).Nonempty :=
  ⟨r, c, hc, hlast, hlen⟩

theorem IsAdditionChain.one_le_of_mem {c : List ℕ} (h : IsAdditionChain c) {x : ℕ}
    (hx : x ∈ c) : 1 ≤ x := byc:List ℕh:IsAdditionChain cx:ℕhx:x ∈ c⊢ 1 ≤ x
  obtain ⟨hhead, hsorted, -⟩ := hc:List ℕx:ℕhx:x ∈ chhead:c.head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) c⊢ 1 ≤ x
  cases c with
  | nil =>nilx:ℕhx:x ∈ []hhead:[].head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) []⊢ 1 ≤ x simp at hxAll goals completed! 🐙
  | cons a t =>consx:ℕa:ℕt:List ℕhx:x ∈ a :: thhead:(a :: t).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (a :: t)⊢ 1 ≤ x
    simp only [List.head?_cons, Option.some.injEq] at hheadconsx:ℕa:ℕt:List ℕhx:x ∈ a :: thsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (a :: t)hhead:a = 1⊢ 1 ≤ x
    subst hheadconsx:ℕt:List ℕhx:x ∈ 1 :: thsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (1 :: t)⊢ 1 ≤ x
    rcases List.mem_cons.mp hx with rfl | hxcons.inlt:List ℕhsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (1 :: t)hx:1 ∈ 1 :: t⊢ 1 ≤ 1cons.inrx:ℕt:List ℕhx✝:x ∈ 1 :: thsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (1 :: t)hx:x ∈ t⊢ 1 ≤ x
    ·cons.inlt:List ℕhsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (1 :: t)hx:1 ∈ 1 :: t⊢ 1 ≤ 1 exact le_rflAll goals completed! 🐙
    ·cons.inrx:ℕt:List ℕhx✝:x ∈ 1 :: thsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (1 :: t)hx:x ∈ t⊢ 1 ≤ x exact le_of_lt ((List.pairwise_cons.mp hsorted).1 _ hx)All goals completed! 🐙

Dropping the last entry of a chain leaves a chain. The entries are positive, so a summand of the last entry is never the last entry itself and so survives the drop.


theorem IsAdditionChain.dropLast {ys : List ℕ} {y : ℕ} (h : IsAdditionChain (ys ++ [y]))
    (hys : ys ≠ []) : IsAdditionChain ys := byys:List ℕy:ℕh:IsAdditionChain (ys ++ [y])hys:ys ≠ []⊢ IsAdditionChain ys
  obtain ⟨hhead, hsorted, hsum⟩ := hys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + z⊢ IsAdditionChain ys
  refine ⟨?_, (List.pairwise_append.mp hsorted).1, ?_⟩refine_1ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + z⊢ ys.head? = some 1refine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + z⊢ ∀ x ∈ ys, x ≠ 1 → ∃ y ∈ ys, ∃ z ∈ ys, x = y + z
  ·refine_1ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + z⊢ ys.head? = some 1 cases ys with
    | nil =>refine_1.nily:ℕhys:[] ≠ []hhead:([] ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) ([] ++ [y])hsum:∀ x ∈ [] ++ [y], x ≠ 1 → ∃ y_1 ∈ [] ++ [y], ∃ z ∈ [] ++ [y], x = y_1 + z⊢ [].head? = some 1 simp at hysAll goals completed! 🐙
    | cons a t =>refine_1.consy:ℕa:ℕt:List ℕhys:a :: t ≠ []hhead:(a :: t ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (a :: t ++ [y])hsum:∀ x ∈ a :: t ++ [y], x ≠ 1 → ∃ y_1 ∈ a :: t ++ [y], ∃ z ∈ a :: t ++ [y], x = y_1 + z⊢ (a :: t).head? = some 1 simpa using hheadAll goals completed! 🐙
  ·refine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + z⊢ ∀ x ∈ ys, x ≠ 1 → ∃ y ∈ ys, ∃ z ∈ ys, x = y + z intro x hx hx1refine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zx:ℕhx:x ∈ yshx1:x ≠ 1⊢ ∃ y ∈ ys, ∃ z ∈ ys, x = y + z
    obtain ⟨a, ha, b, hb, rfl⟩ := hsum x (List.mem_append_left _ hx) hx1refine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z
    have hxy := (List.pairwise_append.mp hsorted).2.2 _ hx _ (List.mem_singleton_self y)refine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z
    have ha1 := IsAdditionChain.one_le_of_mem ⟨hhead, hsorted, hsum⟩ harefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ a⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z
    have hb1 := IsAdditionChain.one_le_of_mem ⟨hhead, hsorted, hsum⟩ hbrefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ b⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z
    have hay : a ≠ y := byys:List ℕy:ℕh:IsAdditionChain (ys ++ [y])hys:ys ≠ []⊢ IsAdditionChain ysrefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z rintro rflys:List ℕhys:ys ≠ []a:ℕb:ℕhx:a + b ∈ yshx1:a + b ≠ 1ha1:1 ≤ ahb1:1 ≤ bhhead:(ys ++ [a]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [a])hsum:∀ x ∈ ys ++ [a], x ≠ 1 → ∃ y ∈ ys ++ [a], ∃ z ∈ ys ++ [a], x = y + zha:a ∈ ys ++ [a]hb:b ∈ ys ++ [a]hxy:a + b < a⊢ Falserefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z; omegarefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + zrefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z
    have hby : b ≠ y := byys:List ℕy:ℕh:IsAdditionChain (ys ++ [y])hys:ys ≠ []⊢ IsAdditionChain ysrefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z rintro rflys:List ℕhys:ys ≠ []a:ℕb:ℕhx:a + b ∈ yshx1:a + b ≠ 1ha1:1 ≤ ahb1:1 ≤ bhhead:(ys ++ [b]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [b])hsum:∀ x ∈ ys ++ [b], x ≠ 1 → ∃ y ∈ ys ++ [b], ∃ z ∈ ys ++ [b], x = y + zha:a ∈ ys ++ [b]hb:b ∈ ys ++ [b]hxy:a + b < bhay:a ≠ b⊢ Falserefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z; omegarefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + zrefine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ ∃ y ∈ ys, ∃ z ∈ ys, a + b = y + z
    refine ⟨a, ?_, b, ?_, rfl⟩refine_2.refine_1ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ a ∈ ysrefine_2.refine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ b ∈ ys
    ·refine_2.refine_1ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ a ∈ ys rcases List.mem_append.mp ha with h | hrefine_2.refine_1.inlys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:a ∈ ys⊢ a ∈ ysrefine_2.refine_1.inrys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:a ∈ [y]⊢ a ∈ ys
      ·refine_2.refine_1.inlys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:a ∈ ys⊢ a ∈ ys exact hAll goals completed! 🐙
      ·refine_2.refine_1.inrys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:a ∈ [y]⊢ a ∈ ys exact absurd (List.mem_singleton.mp h) hayAll goals completed! 🐙
    ·refine_2.refine_2ys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ y⊢ b ∈ ys rcases List.mem_append.mp hb with h | hrefine_2.refine_2.inlys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:b ∈ ys⊢ b ∈ ysrefine_2.refine_2.inrys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:b ∈ [y]⊢ b ∈ ys
      ·refine_2.refine_2.inlys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:b ∈ ys⊢ b ∈ ys exact hAll goals completed! 🐙
      ·refine_2.refine_2.inrys:List ℕy:ℕhys:ys ≠ []hhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + za:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hx:a + b ∈ yshx1:a + b ≠ 1hxy:a + b < yha1:1 ≤ ahb1:1 ≤ bhay:a ≠ yhby:b ≠ yh:b ∈ [y]⊢ b ∈ ys exact absurd (List.mem_singleton.mp h) hbyAll goals completed! 🐙

Every step at most doubles, so a chain of r steps cannot reach past 2 ^ r.


theorem IsAdditionChain.getLast_le_two_pow {c : List ℕ} (h : IsAdditionChain c) (hne : c ≠ []) :
    c.getLast hne ≤ 2 ^ (c.length - 1) := byc:List ℕh:IsAdditionChain chne:c ≠ []⊢ c.getLast hne ≤ 2 ^ (c.length - 1)
  induction c using List.reverseRecOn with
  | nil =>nilh:IsAdditionChain []hne:[] ≠ []⊢ [].getLast hne ≤ 2 ^ ([].length - 1) simp at hneAll goals completed! 🐙
  | append_singleton ys y ih =>append_singletonys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)h:IsAdditionChain (ys ++ [y])hne:ys ++ [y] ≠ []⊢ (ys ++ [y]).getLast hne ≤ 2 ^ ((ys ++ [y]).length - 1)
    rw [List.getLast_append_singletonappend_singletonys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)h:IsAdditionChain (ys ++ [y])hne:ys ++ [y] ≠ []⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)append_singletonys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)h:IsAdditionChain (ys ++ [y])hne:ys ++ [y] ≠ []⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)]append_singletonys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)h:IsAdditionChain (ys ++ [y])hne:ys ++ [y] ≠ []⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
    rcases eq_or_ne ys [] with rfl | hysappend_singleton.inly:ℕih:IsAdditionChain [] → ∀ (hne : [] ≠ []), [].getLast hne ≤ 2 ^ ([].length - 1)h:IsAdditionChain ([] ++ [y])hne:[] ++ [y] ≠ []⊢ y ≤ 2 ^ (([] ++ [y]).length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)h:IsAdditionChain (ys ++ [y])hne:ys ++ [y] ≠ []hys:ys ≠ []⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
    ·append_singleton.inly:ℕih:IsAdditionChain [] → ∀ (hne : [] ≠ []), [].getLast hne ≤ 2 ^ ([].length - 1)h:IsAdditionChain ([] ++ [y])hne:[] ++ [y] ≠ []⊢ y ≤ 2 ^ (([] ++ [y]).length - 1) obtain ⟨hhead, -, -⟩ := happend_singleton.inly:ℕih:IsAdditionChain [] → ∀ (hne : [] ≠ []), [].getLast hne ≤ 2 ^ ([].length - 1)hne:[] ++ [y] ≠ []hhead:([] ++ [y]).head? = some 1⊢ y ≤ 2 ^ (([] ++ [y]).length - 1)
      simp only [List.nil_append, List.head?_cons, Option.some.injEq] at hheadappend_singleton.inly:ℕih:IsAdditionChain [] → ∀ (hne : [] ≠ []), [].getLast hne ≤ 2 ^ ([].length - 1)hne:[] ++ [y] ≠ []hhead:y = 1⊢ y ≤ 2 ^ (([] ++ [y]).length - 1)
      simp [hhead]All goals completed! 🐙
    ·append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)h:IsAdditionChain (ys ++ [y])hne:ys ++ [y] ≠ []hys:ys ≠ []⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) have hchain := h.dropLast hysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)h:IsAdditionChain (ys ++ [y])hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      obtain ⟨hhead, hsorted, hsum⟩ := happend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + z⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hy1 : y ≠ 1 := byc:List ℕh:IsAdditionChain chne:c ≠ []⊢ c.getLast hne ≤ 2 ^ (c.length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        rintro rflys:List ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hys:ys ≠ []hchain:IsAdditionChain yshne:ys ++ [1] ≠ []hhead:(ys ++ [1]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [1])hsum:∀ x ∈ ys ++ [1], x ≠ 1 → ∃ y ∈ ys ++ [1], ∃ z ∈ ys ++ [1], x = y + z⊢ Falseappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        obtain ⟨a, hays⟩ := List.exists_mem_of_ne_nil ys hysys:List ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hys:ys ≠ []hchain:IsAdditionChain yshne:ys ++ [1] ≠ []hhead:(ys ++ [1]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [1])hsum:∀ x ∈ ys ++ [1], x ≠ 1 → ∃ y ∈ ys ++ [1], ∃ z ∈ ys ++ [1], x = y + za:ℕhays:a ∈ ys⊢ Falseappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        have := (List.pairwise_append.mp hsorted).2.2 _ hays _ (List.mem_singleton_self 1)ys:List ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hys:ys ≠ []hchain:IsAdditionChain yshne:ys ++ [1] ≠ []hhead:(ys ++ [1]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [1])hsum:∀ x ∈ ys ++ [1], x ≠ 1 → ∃ y ∈ ys ++ [1], ∃ z ∈ ys ++ [1], x = y + za:ℕhays:a ∈ ysthis:a < 1⊢ Falseappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        have := IsAdditionChain.one_le_of_mem ⟨hhead, hsorted, hsum⟩ (List.mem_append_left _ hays)ys:List ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hys:ys ≠ []hchain:IsAdditionChain yshne:ys ++ [1] ≠ []hhead:(ys ++ [1]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [1])hsum:∀ x ∈ ys ++ [1], x ≠ 1 → ∃ y ∈ ys ++ [1], ∃ z ∈ ys ++ [1], x = y + za:ℕhays:a ∈ ysthis✝:a < 1this:1 ≤ a⊢ Falseappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        omegaappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      obtain ⟨a, ha, b, hb, hyab⟩ := hsum y (byys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1⊢ y ∈ ys ++ [y]append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + b⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) simpAll goals completed! 🐙append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + b⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)) hy1append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + b⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have ha1 := IsAdditionChain.one_le_of_mem ⟨hhead, hsorted, hsum⟩ haappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ a⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hb1 := IsAdditionChain.one_le_of_mem ⟨hhead, hsorted, hsum⟩ hbappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ b⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hays : a ∈ ys := byc:List ℕh:IsAdditionChain chne:c ≠ []⊢ c.getLast hne ≤ 2 ^ (c.length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        rcases List.mem_append.mp ha with h' | h'inlys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bh':a ∈ ys⊢ a ∈ ysinrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bh':a ∈ [y]⊢ a ∈ ysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        ·inlys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bh':a ∈ ys⊢ a ∈ ysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) exact h'All goals completed! 🐙append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        ·inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bh':a ∈ [y]⊢ a ∈ ysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) exact absurd (List.mem_singleton.mp h') (byys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bh':a ∈ [y]⊢ ¬a = yappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) rintro rflys:List ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hys:ys ≠ []hchain:IsAdditionChain ysa:ℕb:ℕha1:1 ≤ ahb1:1 ≤ bhne:ys ++ [a] ≠ []hhead:(ys ++ [a]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [a])hsum:∀ x ∈ ys ++ [a], x ≠ 1 → ∃ y ∈ ys ++ [a], ∃ z ∈ ys ++ [a], x = y + zhy1:a ≠ 1ha:a ∈ ys ++ [a]hb:b ∈ ys ++ [a]hyab:a = a + bh':a ∈ [a]⊢ Falseappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1); omegaAll goals completed! 🐙append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1))append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hbys : b ∈ ys := byc:List ℕh:IsAdditionChain chne:c ≠ []⊢ c.getLast hne ≤ 2 ^ (c.length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        rcases List.mem_append.mp hb with h' | h'inlys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ysh':b ∈ ys⊢ b ∈ ysinrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ysh':b ∈ [y]⊢ b ∈ ysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        ·inlys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ysh':b ∈ ys⊢ b ∈ ysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) exact h'All goals completed! 🐙append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
        ·inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ysh':b ∈ [y]⊢ b ∈ ysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) exact absurd (List.mem_singleton.mp h') (byys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ ysh':b ∈ [y]⊢ ¬b = yappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) rintro rflys:List ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hys:ys ≠ []hchain:IsAdditionChain ysa:ℕb:ℕha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshne:ys ++ [b] ≠ []hhead:(ys ++ [b]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [b])hsum:∀ x ∈ ys ++ [b], x ≠ 1 → ∃ y ∈ ys ++ [b], ∃ z ∈ ys ++ [b], x = y + zhy1:b ≠ 1ha:a ∈ ys ++ [b]hb:b ∈ ys ++ [b]hyab:b = a + bh':b ∈ [b]⊢ Falseappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1); omegaAll goals completed! 🐙append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1))append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hsub := (List.pairwise_append.mp hsorted).1.imp le_of_ltappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) ys⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hla := hsub.rel_getLast haysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hlb := hsub.rel_getLast hbysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hih := ih hchain hysappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      have hlen : (ys ++ [y]).length - 1 = ys.length := byc:List ℕh:IsAdditionChain chne:c ≠ []⊢ c.getLast hne ≤ 2 ^ (c.length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.length⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1) simpappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.length⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.length⊢ y ≤ 2 ^ ((ys ++ [y]).length - 1)
      rw [hlenappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.length⊢ y ≤ 2 ^ ys.lengthappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.length⊢ y ≤ 2 ^ ys.length]append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.length⊢ y ≤ 2 ^ ys.length
      have hyl : ys.length = (ys.length - 1) + 1 := byc:List ℕh:IsAdditionChain chne:c ≠ []⊢ c.getLast hne ≤ 2 ^ (c.length - 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ ys.length
        cases ys with
        | nil =>nily:ℕhy1:y ≠ 1a:ℕb:ℕhyab:y = a + bha1:1 ≤ ahb1:1 ≤ bih:IsAdditionChain [] → ∀ (hne : [] ≠ []), [].getLast hne ≤ 2 ^ ([].length - 1)hne:[] ++ [y] ≠ []hys:[] ≠ []hchain:IsAdditionChain []hhead:([] ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) ([] ++ [y])hsum:∀ x ∈ [] ++ [y], x ≠ 1 → ∃ y_1 ∈ [] ++ [y], ∃ z ∈ [] ++ [y], x = y_1 + zha:a ∈ [] ++ [y]hb:b ∈ [] ++ [y]hays:a ∈ []hbys:b ∈ []hsub:List.Pairwise (fun {a b} ↦ a ≤ b) []hla:a ≤ [].getLast ⋯hlb:b ≤ [].getLast ⋯hih:[].getLast hys ≤ 2 ^ ([].length - 1)hlen:([] ++ [y]).length - 1 = [].length⊢ [].length = [].length - 1 + 1append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ ys.length simp at hysAll goals completed! 🐙append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ ys.length
        | cons _ t =>consy:ℕhy1:y ≠ 1a:ℕb:ℕhyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhead✝:ℕt:List ℕih:IsAdditionChain (head✝ :: t) → ∀ (hne : head✝ :: t ≠ []), (head✝ :: t).getLast hne ≤ 2 ^ ((head✝ :: t).length - 1)hne:head✝ :: t ++ [y] ≠ []hys:head✝ :: t ≠ []hchain:IsAdditionChain (head✝ :: t)hhead:(head✝ :: t ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (head✝ :: t ++ [y])hsum:∀ x ∈ head✝ :: t ++ [y], x ≠ 1 → ∃ y_1 ∈ head✝ :: t ++ [y], ∃ z ∈ head✝ :: t ++ [y], x = y_1 + zha:a ∈ head✝ :: t ++ [y]hb:b ∈ head✝ :: t ++ [y]hays:a ∈ head✝ :: thbys:b ∈ head✝ :: thsub:List.Pairwise (fun {a b} ↦ a ≤ b) (head✝ :: t)hla:a ≤ (head✝ :: t).getLast ⋯hlb:b ≤ (head✝ :: t).getLast ⋯hih:(head✝ :: t).getLast hys ≤ 2 ^ ((head✝ :: t).length - 1)hlen:(head✝ :: t ++ [y]).length - 1 = (head✝ :: t).length⊢ (head✝ :: t).length = (head✝ :: t).length - 1 + 1append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ ys.length simpappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ ys.lengthappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ ys.length
      rw [hyl,append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ (ys.length - 1 + 1)append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ (ys.length - 1) * 2 pow_succappend_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ (ys.length - 1) * 2append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ (ys.length - 1) * 2]append_singleton.inrys:List ℕy:ℕih:IsAdditionChain ys → ∀ (hne : ys ≠ []), ys.getLast hne ≤ 2 ^ (ys.length - 1)hne:ys ++ [y] ≠ []hys:ys ≠ []hchain:IsAdditionChain yshhead:(ys ++ [y]).head? = some 1hsorted:List.Pairwise (fun x1 x2 ↦ x1 < x2) (ys ++ [y])hsum:∀ x ∈ ys ++ [y], x ≠ 1 → ∃ y_1 ∈ ys ++ [y], ∃ z ∈ ys ++ [y], x = y_1 + zhy1:y ≠ 1a:ℕha:a ∈ ys ++ [y]b:ℕhb:b ∈ ys ++ [y]hyab:y = a + bha1:1 ≤ ahb1:1 ≤ bhays:a ∈ yshbys:b ∈ yshsub:List.Pairwise (fun {a b} ↦ a ≤ b) yshla:a ≤ ys.getLast ⋯hlb:b ≤ ys.getLast ⋯hih:ys.getLast hys ≤ 2 ^ (ys.length - 1)hlen:(ys ++ [y]).length - 1 = ys.lengthhyl:ys.length = ys.length - 1 + 1⊢ y ≤ 2 ^ (ys.length - 1) * 2
      omegaAll goals completed! 🐙

The doubling bound, transported to ℓ: reaching n takes at least log₂ n steps.


theorem le_two_pow_additionChainLength {n : ℕ} (hne : (additionChainSteps n).Nonempty) :
    n ≤ 2 ^ additionChainLength n := byn:ℕhne:(additionChainSteps n).Nonempty⊢ n ≤ 2 ^ additionChainLength n
  obtain ⟨c, hc, hlast, hlen⟩ := Nat.sInf_mem hnen:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1⊢ n ≤ 2 ^ additionChainLength n
  have hcne : c ≠ [] := by rintro rfln:ℕhne:(additionChainSteps n).Nonemptyhc:IsAdditionChain []hlast:[].getLast? = some nhlen:[].length = sInf (additionChainSteps n) + 1⊢ Falsen:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []⊢ n ≤ 2 ^ additionChainLength n; simp at hlastn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []⊢ n ≤ 2 ^ additionChainLength nn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []⊢ n ≤ 2 ^ additionChainLength n
  have : c.getLast hcne = n := by
    rw [List.getLast?_eq_some_getLast (l := c) (h := hcne)n:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []hlast:some (c.getLast hcne) = some n⊢ c.getLast hcne = nn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []hlast:some (c.getLast hcne) = some n⊢ c.getLast hcne = nn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this:c.getLast hcne = n⊢ n ≤ 2 ^ additionChainLength n] at hlastn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []hlast:some (c.getLast hcne) = some n⊢ c.getLast hcne = nn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this:c.getLast hcne = n⊢ n ≤ 2 ^ additionChainLength n
    exact Option.some.inj hlastn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this:c.getLast hcne = n⊢ n ≤ 2 ^ additionChainLength nn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this:c.getLast hcne = n⊢ n ≤ 2 ^ additionChainLength n
  have := hc.getLast_le_two_pow hcnen:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this✝:c.getLast hcne = nthis:c.getLast hcne ≤ 2 ^ (c.length - 1)⊢ n ≤ 2 ^ additionChainLength n
  rw [‹c.getLast hcne = n›,n:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this✝:c.getLast hcne = nthis:n ≤ 2 ^ (c.length - 1)⊢ n ≤ 2 ^ additionChainLength nn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this✝:c.getLast hcne = nthis:n ≤ 2 ^ (sInf (additionChainSteps n) + 1 - 1)⊢ n ≤ 2 ^ additionChainLength n hlenn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this✝:c.getLast hcne = nthis:n ≤ 2 ^ (sInf (additionChainSteps n) + 1 - 1)⊢ n ≤ 2 ^ additionChainLength nn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this✝:c.getLast hcne = nthis:n ≤ 2 ^ (sInf (additionChainSteps n) + 1 - 1)⊢ n ≤ 2 ^ additionChainLength n] at thisn:ℕhne:(additionChainSteps n).Nonemptyc:List ℕhc:IsAdditionChain chlast:c.getLast? = some nhlen:c.length = sInf (additionChainSteps n) + 1hcne:c ≠ []this✝:c.getLast hcne = nthis:n ≤ 2 ^ (sInf (additionChainSteps n) + 1 - 1)⊢ n ≤ 2 ^ additionChainLength n
  simpa [additionChainLength_eq_sInf] using thisAll goals completed! 🐙

The lower-bound tool: r steps cannot reach past 2 ^ r.


theorem lt_additionChainLength_of_two_pow_lt {n r : ℕ} (hne : (additionChainSteps n).Nonempty)
    (h : 2 ^ r < n) : r < additionChainLength n := byn:ℕr:ℕhne:(additionChainSteps n).Nonemptyh:2 ^ r < n⊢ r < additionChainLength n
  by_contra! hconn:ℕr:ℕhne:(additionChainSteps n).Nonemptyh:2 ^ r < nhcon:additionChainLength n ≤ r⊢ False
  have h1 := le_two_pow_additionChainLength hnen:ℕr:ℕhne:(additionChainSteps n).Nonemptyh:2 ^ r < nhcon:additionChainLength n ≤ rh1:n ≤ 2 ^ additionChainLength n⊢ False
  have h2 : (2 : ℕ) ^ additionChainLength n ≤ 2 ^ r := Nat.pow_le_pow_right (byn:ℕr:ℕhne:(additionChainSteps n).Nonemptyh:2 ^ r < nhcon:additionChainLength n ≤ rh1:n ≤ 2 ^ additionChainLength n⊢ 2 > 0n:ℕr:ℕhne:(additionChainSteps n).Nonemptyh:2 ^ r < nhcon:additionChainLength n ≤ rh1:n ≤ 2 ^ additionChainLength nh2:2 ^ additionChainLength n ≤ 2 ^ r⊢ False omegaAll goals completed! 🐙n:ℕr:ℕhne:(additionChainSteps n).Nonemptyh:2 ^ r < nhcon:additionChainLength n ≤ rh1:n ≤ 2 ^ additionChainLength nh2:2 ^ additionChainLength n ≤ 2 ^ r⊢ False) hconn:ℕr:ℕhne:(additionChainSteps n).Nonemptyh:2 ^ r < nhcon:additionChainLength n ≤ rh1:n ≤ 2 ^ additionChainLength nh2:2 ^ additionChainLength n ≤ 2 ^ r⊢ False
  omegaAll goals completed! 🐙