import Pretty.Defs.Factory
import Pretty.Tactic

/-!
## The cost factory for SnowWhite
-/

def maxw: ℕ
maxw : ℕ: Type
ℕ := 80: ?m.4
80 

/--
The cost factory for SnowWhite (Section 6) along with proofs that 
the operations satisfy the contracts imposed by the cost factory interface.
-/
def ourFactory: Factory (ℕ × ℕ)
ourFactory : Factory: Type → Type
Factory (ℕ: Type
ℕ × ℕ: Type
ℕ) := 
  {
    le := fun ⟨sumo₁: ℕ
sumo₁, h₁: ℕ
h₁⟩ ⟨sumo₂: ℕ
sumo₂, h₂: ℕ
h₂⟩ => 
      if sumo₁: ℕ
sumo₁ = sumo₂: ℕ
sumo₂ then 
        h₁: ℕ
h₁ ≤ h₂: ℕ
h₂ 
      else 
        sumo₁: ℕ
sumo₁ < sumo₂: ℕ
sumo₂,

    concat := fun ⟨sumo₁: ℕ
sumo₁, h₁: ℕ
h₁⟩ ⟨sumo₂: ℕ
sumo₂, h₂: ℕ
h₂⟩ => ⟨sumo₁: ℕ
sumo₁ + sumo₂: ℕ
sumo₂, h₁: ℕ
h₁ + h₂: ℕ
h₂⟩,
    
    text := fun c: ?m.500
c l: ?m.503
l => 
      let a: ?m.506
a := (max: {α : Type ?u.510} → [self : Max α] → α → α → α
max maxw: ℕ
maxw c: ?m.500
c) - maxw: ℕ
maxw 
      let b: ?m.566
b := c: ?m.500
c + l: ?m.503
l - (max: {α : Type ?u.573} → [self : Max α] → α → α → α
max maxw: ℕ
maxw c: ?m.500
c)
      ⟨b: ?m.566
b * (2: ?m.638
2 * a: ?m.506
a + b: ?m.566
b), 0: ?m.743
0⟩,

    nl := fun _: ?m.766
_ => ⟨0: ?m.777
0, 1: ?m.780
1⟩,
    W := 100: ?m.789
100,

    text_monotonic := by
Goals accomplished! 🐙 
∀ {c c' l : ℕ},
  c ≤ c' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c l)
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c' l) =       true{
∀ {c c' l : ℕ},
  c ≤ c' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c l)
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c' l) =       true
      
∀ {c c' l : ℕ},
  c ≤ c' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c l)
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c' l) =       trueintros c: ℕ
c c': ℕ
c' l: ℕ
l hc: c ≤ c'
hcc, c', l: ℕ

hc: c ≤ c'

(fun x x_1 =>
      match x with
      | (sumo₁, h₁) =>
        match x_1 with
        | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
    ((fun c l =>
        let a := max maxw c - maxw;
        let b := c + l - max maxw c;
        (b * (2 * a + b), 0))
      c l)
    ((fun c l =>
        let a := max maxw c - maxw;
        let b := c + l - max maxw c;
        (b * (2 * a + b), 0))
      c' l) =   true 
      
∀ {c c' l : ℕ},
  c ≤ c' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c l)
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c' l) =       truesimpc, c', l: ℕ

hc: c ≤ c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) 
      
∀ {c c' l : ℕ},
  c ≤ c' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c l)
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c' l) =       trueby_cases h_l: ?m.12432
h_l : l: ℕ
l > 0: ?m.12386
0c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

pos¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
c, c', l: ℕ

hc: c ≤ c'

h_l: ¬l > 0

neg¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) 
      
∀ {c c' l : ℕ},
  c ≤ c' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c l)
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c' l) =       truecase pos => 
        c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by_cases h_if0: ?m.12466
h_if0 : c: ℕ
c = c': ℕ
c'c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: c = c'

pos¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

neg¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) 
        c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case pos => c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: c = c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp [h_if0: ?m.12466
h_if0]
Goals accomplished! 🐙
        c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case neg => 
          c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))have h_lt: c < c'
h_lt : c: ℕ
c < c': ℕ
c' := c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by
Goals accomplished! 🐙 c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

c < c'{c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

c < c'
            c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

c < c'simp at h_if0: ¬c = c'
h_if0c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

c < c' 
            c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

c < c'cases hc: c ≤ c'
hcc, l: ℕ

h_l: l > 0

h_if0: ¬c = c

reflc < c
c, l: ℕ

h_l: l > 0

m✝: ℕ

a✝: Nat.le c m✝

h_if0: ¬c = Nat.succ m✝

stepc < Nat.succ m✝ 
            c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

c < c'case refl => c, l: ℕ

h_l: l > 0

h_if0: ¬c = c

c < csimp at h_if0: ¬c = c
h_if0
Goals accomplished! 🐙
            c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

c < c'case step => 
              c, l: ℕ

h_l: l > 0

m✝: ℕ

a✝: Nat.le c m✝

h_if0: ¬c = Nat.succ m✝

c < Nat.succ m✝simp_arith at *c, l, m✝: ℕ

a✝: c ≤ m✝

h_l: 1 ≤ l

h_if0: ¬c = m✝ + 1

c ≤ m✝
              c, l: ℕ

h_l: l > 0

m✝: ℕ

a✝: Nat.le c m✝

h_if0: ¬c = Nat.succ m✝

c < Nat.succ m✝assumption
Goals accomplished! 🐙
          }
Goals accomplished! 🐙
          c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))clear hc: c ≤ c'
hc h_if0: ?m.12473
h_if0c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
          c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by_cases h_if: ?m.26335
h_if : c: ℕ
c ≥ maxw: ℕ
maxwc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

pos¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: ¬c ≥ maxw

neg¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
          c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case pos => 
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))have h_if': c' ≥ maxw
h_if' : c': ℕ
c' ≥ maxw: ℕ
maxw := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

c' ≥ maxwlinarith
Goals accomplished! 🐙
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp [h_if: ?m.26335
h_if, h_if': c' ≥ maxw
h_if']c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

¬(c - maxw = c' - maxw ∨ l = 0) → l * (2 * (c - maxw) + l) < l * (2 * (c' - maxw) + l)
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))intro h: ¬(c - maxw = c' - maxw ∨ l = 0)
hc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

l * (2 * (c - maxw) + l) < l * (2 * (c' - maxw) + l) 
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))apply Nat.mul_lt_mul_of_pos_left: ∀ {n m k : ℕ}, n < m → k > 0 → k * n < k * m
Nat.mul_lt_mul_of_pos_leftc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

h2 * (c - maxw) + l < 2 * (c' - maxw) + l
c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

hkl > 0
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case h => 
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

2 * (c - maxw) + l < 2 * (c' - maxw) + lapply Nat.add_lt_add_right: ∀ {n m : ℕ}, n < m → ∀ (k : ℕ), n + k < m + k
Nat.add_lt_add_rightc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

h2 * (c - maxw) < 2 * (c' - maxw)
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

2 * (c - maxw) + l < 2 * (c' - maxw) + lapply Nat.mul_lt_mul_of_pos_left: ∀ {n m k : ℕ}, n < m → k > 0 → k * n < k * m
Nat.mul_lt_mul_of_pos_leftc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

h.hc - maxw < c' - maxw
c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

h.hk2 > 0
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

2 * (c - maxw) + l < 2 * (c' - maxw) + lcase h => 
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

c - maxw < c' - maxwclear h: ¬(c - maxw = c' - maxw ∨ l = 0)
h h_l: ?m.12432
h_lc, c', l: ℕ

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

c - maxw < c' - maxw
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

c - maxw < c' - maxwdwi { c, c', l: ℕ

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

c - maxw < c' - maxwapply Nat.sub_lt_sub_right: ∀ {a b c : ℕ}, a < b → c ≤ a → a - c < b - c
Nat.sub_lt_sub_rightc, c', l: ℕ

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h0c < c'
c, c', l: ℕ

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h1maxw ≤ c }
Goals accomplished! 🐙
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

2 * (c - maxw) + l < 2 * (c' - maxw) + lcase hk => c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

2 > 0simp
Goals accomplished! 🐙
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case hk => c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c ≥ maxw

h_if': c' ≥ maxw

h: ¬(c - maxw = c' - maxw ∨ l = 0)

l > 0assumption
Goals accomplished! 🐙
          c, c', l: ℕ

hc: c ≤ c'

h_l: l > 0

h_if0: ¬c = c'

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case neg => 
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: ¬c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp at h_if: ?m.26342
h_ifc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) 
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: ¬c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))have h_max: max maxw c = maxw
h_max : max: {α : Type ?u.38340} → [self : Max α] → α → α → α
max maxw: ℕ
maxw c: ℕ
c = maxw: ℕ
maxw := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

max maxw c = maxw{c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

max maxw c = maxw
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

max maxw c = maxwsimpc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

c ≤ maxw 
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

max maxw c = maxwapply Nat.le_of_lt: ∀ {n m : ℕ}, n < m → n ≤ m
Nat.le_of_ltc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

hc < maxw
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

max maxw c = maxwassumption
Goals accomplished! 🐙
            }
Goals accomplished! 🐙
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: ¬c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp [h_max: max maxw c = maxw
h_max]c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: ¬c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by_cases h_if': ?m.49328
h_if' : c': ℕ
c' ≥ maxw: ℕ
maxwc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

pos¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

neg¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: ¬c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case pos => 
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp [h_if': ?m.49328
h_if']c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l) →
  (c + l - maxw) * (c + l - maxw) < l * (2 * (c' - maxw) + l)
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))intro _: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)
_c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

(c + l - maxw) * (c + l - maxw) < l * (2 * (c' - maxw) + l)
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))have : c: ℕ
c + l: ℕ
l - maxw: ℕ
maxw < l: ℕ
l := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

(c + l - maxw) * (c + l - maxw) < l * (2 * (c' - maxw) + l)by
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

c + l - maxw < l{c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

c + l - maxw < l
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

c + l - maxw < lclear * - h_if: c < maxw
h_if h_l: l > 0
h_lc, l: ℕ

h_l: l > 0

h_if: c < maxw

c + l - maxw < l
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

c + l - maxw < lrw [c, l: ℕ

h_l: l > 0

h_if: c < maxw

c + l - maxw < lNat.add_comm: ∀ (n m : ℕ), n + m = m + n
Nat.add_comm,c, l: ℕ

h_l: l > 0

h_if: c < maxw

l + c - maxw < l c, l: ℕ

h_l: l > 0

h_if: c < maxw

c + l - maxw < lNat.sub_sub_eq: ∀ {a b c : ℕ}, a ≤ b → c + a - b = c - (b - a)
Nat.sub_sub_eqc, l: ℕ

h_l: l > 0

h_if: c < maxw

l - (maxw - c) < l
c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxw]c, l: ℕ

h_l: l > 0

h_if: c < maxw

l - (maxw - c) < l
c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxw
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

c + l - maxw < l. c, l: ℕ

h_l: l > 0

h_if: c < maxw

l - (maxw - c) < l
c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxwgeneralize h : maxw: ℕ
maxw - c: ℕ
c = vc, l: ℕ

h_l: l > 0

h_if: c < maxw

v: ℕ

h: maxw - c = v

l - v < l 
                  c, l: ℕ

h_l: l > 0

h_if: c < maxw

l - (maxw - c) < l
c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxwcases v: ℕ
vc, l: ℕ

h_l: l > 0

h_if: c < maxw

h: maxw - c = Nat.zero

zerol - Nat.zero < l
c, l: ℕ

h_l: l > 0

h_if: c < maxw

n✝: ℕ

h: maxw - c = Nat.succ n✝

succl - Nat.succ n✝ < l 
                  c, l: ℕ

h_l: l > 0

h_if: c < maxw

l - (maxw - c) < l
c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxwcase zero => 
                    c, l: ℕ

h_l: l > 0

h_if: c < maxw

h: maxw - c = Nat.zero

l - Nat.zero < lsimp at h: maxw - c = Nat.zero
hc, l: ℕ

h_l: l > 0

h_if: c < maxw

h: maxw ≤ c

l - Nat.zero < l
                    c, l: ℕ

h_l: l > 0

h_if: c < maxw

h: maxw - c = Nat.zero

l - Nat.zero < llinarith
Goals accomplished! 🐙
                  c, l: ℕ

h_l: l > 0

h_if: c < maxw

l - (maxw - c) < l
c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxwcase succ => 
                    c, l: ℕ

h_l: l > 0

h_if: c < maxw

n✝: ℕ

h: maxw - c = Nat.succ n✝

l - Nat.succ n✝ < lclear * - h_l: l > 0
h_ll: ℕ

h_l: l > 0

n✝: ℕ

l - Nat.succ n✝ < l
                    c, l: ℕ

h_l: l > 0

h_if: c < maxw

n✝: ℕ

h: maxw - c = Nat.succ n✝

l - Nat.succ n✝ < lcases l: ℕ
ln✝: ℕ

h_l: Nat.zero > 0

zeroNat.zero - Nat.succ n✝ < Nat.zero
n✝¹, n✝: ℕ

h_l: Nat.succ n✝ > 0

succNat.succ n✝ - Nat.succ n✝¹ < Nat.succ n✝ 
                    c, l: ℕ

h_l: l > 0

h_if: c < maxw

n✝: ℕ

h: maxw - c = Nat.succ n✝

l - Nat.succ n✝ < lcase zero => n✝: ℕ

h_l: Nat.zero > 0

Nat.zero - Nat.succ n✝ < Nat.zerosimp at h_l: Nat.zero > 0
h_l
Goals accomplished! 🐙 
                    c, l: ℕ

h_l: l > 0

h_if: c < maxw

n✝: ℕ

h: maxw - c = Nat.succ n✝

l - Nat.succ n✝ < lcase succ => n✝¹, n✝: ℕ

h_l: Nat.succ n✝ > 0

Nat.succ n✝ - Nat.succ n✝¹ < Nat.succ n✝simp_arith
Goals accomplished! 🐙
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

c + l - maxw < l. c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxwapply Nat.le_of_lt: ∀ {n m : ℕ}, n < m → n ≤ m
Nat.le_of_ltc, l: ℕ

h_l: l > 0

h_if: c < maxw

hc < maxw
                  c, l: ℕ

h_l: l > 0

h_if: c < maxw

c ≤ maxwassumption
Goals accomplished! 🐙
              }
Goals accomplished! 🐙
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))have this2: c + l - maxw < 2 * (c' - maxw) + l
this2 : c: ℕ
c + l: ℕ
l - maxw: ℕ
maxw < 2: ?m.60398
2 * (c': ℕ
c' - maxw: ℕ
maxw) + l: ℕ
l := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

this: c + l - maxw < l

(c + l - maxw) * (c + l - maxw) < l * (2 * (c' - maxw) + l)by
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

this: c + l - maxw < l

c + l - maxw < 2 * (c' - maxw) + llinarith
Goals accomplished! 🐙
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))dwi { c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

this: c + l - maxw < l

this2: c + l - maxw < 2 * (c' - maxw) + l

(c + l - maxw) * (c + l - maxw) < l * (2 * (c' - maxw) + l)apply Nat.mul_lt_mul₀: ∀ {a b c d : ℕ}, a < c → b < d → a * b < c * d
Nat.mul_lt_mul₀c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

this: c + l - maxw < l

this2: c + l - maxw < 2 * (c' - maxw) + l

h1c + l - maxw < l
c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' ≥ maxw

a✝: ¬(c + l - maxw) * (c + l - maxw) = l * (2 * (c' - maxw) + l)

this: c + l - maxw < l

this2: c + l - maxw < 2 * (c' - maxw) + l

h2c + l - maxw < 2 * (c' - maxw) + l }
Goals accomplished! 🐙
            c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: ¬c ≥ maxw

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case neg => 
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp at h_if': ?m.49335
h_if'c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))have h_max': max maxw c' = maxw
h_max' : max: {α : Type ?u.72687} → [self : Max α] → α → α → α
max maxw: ℕ
maxw c': ℕ
c' = maxw: ℕ
maxw := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

max maxw c' = maxw{c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

max maxw c' = maxw
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

max maxw c' = maxwsimpc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

c' ≤ maxw 
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

max maxw c' = maxwapply Nat.le_of_lt: ∀ {n m : ℕ}, n < m → n ≤ m
Nat.le_of_ltc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

hc' < maxw
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

max maxw c' = maxwassumption
Goals accomplished! 🐙
              }
Goals accomplished! 🐙
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp [h_max': max maxw c' = maxw
h_max']c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - maxw) * (c' + l - maxw)
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))intro h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)
hc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

(c + l - maxw) * (c + l - maxw) < (c' + l - maxw) * (c' + l - maxw) 
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))apply Nat.mul_self_lt_mul_self: ∀ {m n : ℕ}, m < n → m * m < n * n
Nat.mul_self_lt_mul_selfc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

ac + l - maxw < c' + l - maxw
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))by_cases h_if'': ?m.80413
h_if'' : c: ℕ
c + l: ℕ
l ≥ maxw: ℕ
maxwc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l ≥ maxw

posc + l - maxw < c' + l - maxw
c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': ¬c + l ≥ maxw

negc + l - maxw < c' + l - maxw
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case pos => 
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l ≥ maxw

c + l - maxw < c' + l - maxwhave h_if''': c' + l ≥ maxw
h_if''' : c': ℕ
c' + l: ℕ
l ≥ maxw: ℕ
maxw := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l ≥ maxw

c + l - maxw < c' + l - maxwby
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l ≥ maxw

c' + l ≥ maxwlinarith
Goals accomplished! 🐙
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l ≥ maxw

c + l - maxw < c' + l - maxwclear * - h_if''': c' + l ≥ maxw
h_if''' h_if'': ?m.80413
h_if'' h_lt: c < c'
h_ltc, c', l: ℕ

h_lt: c < c'

h_if'': c + l ≥ maxw

h_if''': c' + l ≥ maxw

c + l - maxw < c' + l - maxw
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l ≥ maxw

c + l - maxw < c' + l - maxwdwi { c, c', l: ℕ

h_lt: c < c'

h_if'': c + l ≥ maxw

h_if''': c' + l ≥ maxw

c + l - maxw < c' + l - maxwapply Nat.sub_lt_sub_right: ∀ {a b c : ℕ}, a < b → c ≤ a → a - c < b - c
Nat.sub_lt_sub_rightc, c', l: ℕ

h_lt: c < c'

h_if'': c + l ≥ maxw

h_if''': c' + l ≥ maxw

h0c + l < c' + l
c, c', l: ℕ

h_lt: c < c'

h_if'': c + l ≥ maxw

h_if''': c' + l ≥ maxw

h1maxw ≤ c + l }c, c', l: ℕ

h_lt: c < c'

h_if'': c + l ≥ maxw

h_if''': c' + l ≥ maxw

h0c + l < c' + l
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l ≥ maxw

c + l - maxw < c' + l - maxwsimpa
Goals accomplished! 🐙
              c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': ¬c' ≥ maxw

¬(c + l - maxw) * (c + l - maxw) = (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - maxw) * (c + l - maxw) < (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))case neg => 
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': ¬c + l ≥ maxw

c + l - maxw < c' + l - maxwsimp at h_if'': ?m.80420
h_if''c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l - maxw < c' + l - maxw
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': ¬c + l ≥ maxw

c + l - maxw < c' + l - maxwhave : c: ℕ
c + l: ℕ
l - maxw: ℕ
maxw = 0: ?m.85461
0 := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l - maxw < c' + l - maxwby
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l - maxw = 0{c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l - maxw = 0
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l - maxw = 0simpc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l ≤ maxw
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l - maxw = 0apply Nat.le_of_lt: ∀ {n m : ℕ}, n < m → n ≤ m
Nat.le_of_ltc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

hc + l < maxw
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

c + l - maxw = 0assumption
Goals accomplished! 🐙
                }
Goals accomplished! 🐙
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': ¬c + l ≥ maxw

c + l - maxw < c' + l - maxwby_cases h_if''': ?m.86844
h_if''' : c': ℕ
c' + l: ℕ
l > maxw: ℕ
maxwc, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l > maxw

posc + l - maxw < c' + l - maxw
c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': ¬c' + l > maxw

negc + l - maxw < c' + l - maxw 
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': ¬c + l ≥ maxw

c + l - maxw < c' + l - maxwcase pos => 
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l > maxw

c + l - maxw < c' + l - maxwsimp [this: c + l - maxw = 0
this]c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l > maxw

maxw < c' + l
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l > maxw

c + l - maxw < c' + l - maxwsimp at h_if''': ?m.86844
h_if'''c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': maxw < c' + l

maxw < c' + l 
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l > maxw

c + l - maxw < c' + l - maxwassumption
Goals accomplished! 🐙
                c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': ¬c + l ≥ maxw

c + l - maxw < c' + l - maxwcase neg => 
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': ¬c' + l > maxw

c + l - maxw < c' + l - maxwsimp at h_if''': ?m.86851
h_if'''c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l ≤ maxw

c + l - maxw < c' + l - maxw
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': ¬c' + l > maxw

c + l - maxw < c' + l - maxwhave : c': ℕ
c' + l: ℕ
l - maxw: ℕ
maxw = 0: ?m.89584
0 := c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l ≤ maxw

c + l - maxw < c' + l - maxwby
Goals accomplished! 🐙 c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l ≤ maxw

c' + l - maxw = 0{c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l ≤ maxw

c' + l - maxw = 0
                    c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': c' + l ≤ maxw

c' + l - maxw = 0simpa
Goals accomplished! 🐙
                  }
Goals accomplished! 🐙
                  c, c', l: ℕ

h_l: l > 0

h_lt: c < c'

h_if: c < maxw

h_max: max maxw c = maxw

h_if': c' < maxw

h_max': max maxw c' = maxw

h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)

h_if'': c + l < maxw

this: c + l - maxw = 0

h_if''': ¬c' + l > maxw

c + l - maxw < c' + l - maxwsimp [*] at h: ¬(c + l - maxw) * (c + l - maxw) = (c' + l - maxw) * (c' + l - maxw)
h
Goals accomplished! 🐙
      
∀ {c c' l : ℕ},
  c ≤ c' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c l)
        ((fun c l =>
            let a := max maxw c - maxw;
            let b := c + l - max maxw c;
            (b * (2 * a + b), 0))
          c' l) =       truecase neg => 
        c, c', l: ℕ

hc: c ≤ c'

h_l: ¬l > 0

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))intro h: ¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
hc, c', l: ℕ

hc: c ≤ c'

h_l: ¬l > 0

h: ¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))

(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <   (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
        c, c', l: ℕ

hc: c ≤ c'

h_l: ¬l > 0

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp at h_l: ?m.12439
h_lc, c', l: ℕ

hc: c ≤ c'

h: ¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))

h_l: l = 0

(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <   (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) 
        c, c', l: ℕ

hc: c ≤ c'

h_l: ¬l > 0

¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =       (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c')) →
  (c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) <     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))simp [h_l: l = 0
h_l] at h: ¬(c + l - max maxw c) * (2 * (max maxw c - maxw) + (c + l - max maxw c)) =     (c' + l - max maxw c') * (2 * (max maxw c' - maxw) + (c' + l - max maxw c'))
h
Goals accomplished! 🐙 
    }
Goals accomplished! 🐙,

    nl_monotonic := by
Goals accomplished! 🐙 
∀ {i i' : ℕ},
  i ≤ i' →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun x => (0, 1)) i) ((fun x => (0, 1)) i') =       truesimp
Goals accomplished! 🐙,
    concat_monotonic := by
Goals accomplished! 🐙 
∀ {cost₁ cost₂ cost₃ cost₄ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        cost₁ cost₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          cost₃ cost₄ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₁ cost₃)
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₂ cost₄) =         true{
∀ {cost₁ cost₂ cost₃ cost₄ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        cost₁ cost₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          cost₃ cost₄ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₁ cost₃)
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₂ cost₄) =         true
      
∀ {cost₁ cost₂ cost₃ cost₄ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        cost₁ cost₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          cost₃ cost₄ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₁ cost₃)
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₂ cost₄) =         trueintro ⟨sumo₁: ℕ
sumo₁, h₁: ℕ
h₁⟩ ⟨sumo₂: ℕ
sumo₂, h₂: ℕ
h₂⟩ ⟨sumo₃: ℕ
sumo₃, h₃: ℕ
h₃⟩ ⟨sumo₄: ℕ
sumo₄, h₄: ℕ
h₄⟩sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

(fun x x_1 =>
        match x with
        | (sumo₁, h₁) =>
          match x_1 with
          | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
      (sumo₁, h₁) (sumo₂, h₂) =     true →
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        (sumo₃, h₃) (sumo₄, h₄) =       true →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        ((fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
          (sumo₁, h₁) (sumo₃, h₃))
        ((fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
          (sumo₂, h₂) (sumo₄, h₄)) =       true
      
∀ {cost₁ cost₂ cost₃ cost₄ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        cost₁ cost₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          cost₃ cost₄ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₁ cost₃)
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₂ cost₄) =         truesimpsumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

(if sumo₁ = sumo₂ then h₁ ≤ h₂ else sumo₁ < sumo₂) →
  (if sumo₃ = sumo₄ then h₃ ≤ h₄ else sumo₃ < sumo₄) →
    if sumo₁ + sumo₃ = sumo₂ + sumo₄ then h₁ + h₃ ≤ h₂ + h₄ else sumo₁ + sumo₃ < sumo₂ + sumo₄ 
      
∀ {cost₁ cost₂ cost₃ cost₄ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        cost₁ cost₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          cost₃ cost₄ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₁ cost₃)
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₂ cost₄) =         truesplit_ifssumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

inl.inl.inlh₁ ≤ h₂ → h₃ ≤ h₄ → h₁ + h₃ ≤ h₂ + h₄
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: sumo₃ = sumo₄

h✝: ¬sumo₁ + sumo₃ = sumo₂ + sumo₄

inl.inl.inrh₁ ≤ h₂ → h₃ ≤ h₄ → sumo₁ + sumo₃ < sumo₂ + sumo₄
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: ¬sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

inl.inr.inlh₁ ≤ h₂ → sumo₃ < sumo₄ → h₁ + h₃ ≤ h₂ + h₄
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: ¬sumo₃ = sumo₄

h✝: ¬sumo₁ + sumo₃ = sumo₂ + sumo₄

inl.inr.inrh₁ ≤ h₂ → sumo₃ < sumo₄ → sumo₁ + sumo₃ < sumo₂ + sumo₄
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

inr.inl.inlsumo₁ < sumo₂ → h₃ ≤ h₄ → h₁ + h₃ ≤ h₂ + h₄
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: sumo₃ = sumo₄

h✝: ¬sumo₁ + sumo₃ = sumo₂ + sumo₄

inr.inl.inrsumo₁ < sumo₂ → h₃ ≤ h₄ → sumo₁ + sumo₃ < sumo₂ + sumo₄
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: ¬sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

inr.inr.inlsumo₁ < sumo₂ → sumo₃ < sumo₄ → h₁ + h₃ ≤ h₂ + h₄
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: ¬sumo₃ = sumo₄

h✝: ¬sumo₁ + sumo₃ = sumo₂ + sumo₄

inr.inr.inrsumo₁ < sumo₂ → sumo₃ < sumo₄ → sumo₁ + sumo₃ < sumo₂ + sumo₄ 
      
∀ {cost₁ cost₂ cost₃ cost₄ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        cost₁ cost₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          cost₃ cost₄ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₁ cost₃)
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₂ cost₄) =         truecase inl.inl.inl | inr.inr.inl | inr.inr.inr | inr.inl.inr => 
        sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

h₁ ≤ h₂ → h₃ ≤ h₄ → h₁ + h₃ ≤ h₂ + h₄intro h1: sumo₁ < sumo₂
h1 h2: h₃ ≤ h₄
h2sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

h1: h₁ ≤ h₂

h2: h₃ ≤ h₄

h₁ + h₃ ≤ h₂ + h₄ 
        sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: ¬sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

sumo₁ < sumo₂ → sumo₃ < sumo₄ → h₁ + h₃ ≤ h₂ + h₄linarith
Goals accomplished! 🐙
      
∀ {cost₁ cost₂ cost₃ cost₄ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        cost₁ cost₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          cost₃ cost₄ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₁ cost₃)
          ((fun x x_1 =>
              match x with
              | (sumo₁, h₁) =>
                match x_1 with
                | (sumo₂, h₂) => (sumo₁ + sumo₂, h₁ + h₂))
            cost₂ cost₄) =         truecase inl.inl.inr | inl.inr.inl | inl.inr.inr | inr.inl.inl => 
        sumo₁, h₁, sumo₂, h₂, sumo₃, h₃, sumo₄, h₄: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: ¬sumo₃ = sumo₄

h✝: sumo₁ + sumo₃ = sumo₂ + sumo₄

h₁ ≤ h₂ → sumo₃ < sumo₄ → h₁ + h₃ ≤ h₂ + h₄simp [*] at *
Goals accomplished! 🐙
    }
Goals accomplished! 🐙,
    le_trans := by
Goals accomplished! 🐙 
∀ {c₁ c₂ c₃ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₃ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₁ c₃ =         true{
∀ {c₁ c₂ c₃ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₃ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₁ c₃ =         true
      
∀ {c₁ c₂ c₃ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₃ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₁ c₃ =         trueintro ⟨sumo₁: ℕ
sumo₁, h₁: ℕ
h₁⟩ ⟨sumo₂: ℕ
sumo₂, h₂: ℕ
h₂⟩ ⟨sumo₃: ℕ
sumo₃, h₃: ℕ
h₃⟩sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

(fun x x_1 =>
        match x with
        | (sumo₁, h₁) =>
          match x_1 with
          | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
      (sumo₁, h₁) (sumo₂, h₂) =     true →
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        (sumo₂, h₂) (sumo₃, h₃) =       true →
    (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        (sumo₁, h₁) (sumo₃, h₃) =       true
      
∀ {c₁ c₂ c₃ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₃ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₁ c₃ =         truesimpsumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

(if sumo₁ = sumo₂ then h₁ ≤ h₂ else sumo₁ < sumo₂) →
  (if sumo₂ = sumo₃ then h₂ ≤ h₃ else sumo₂ < sumo₃) → if sumo₁ = sumo₃ then h₁ ≤ h₃ else sumo₁ < sumo₃
      
∀ {c₁ c₂ c₃ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₃ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₁ c₃ =         truesplit_ifssumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: sumo₂ = sumo₃

h✝: sumo₁ = sumo₃

inl.inl.inlh₁ ≤ h₂ → h₂ ≤ h₃ → h₁ ≤ h₃
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: sumo₂ = sumo₃

h✝: ¬sumo₁ = sumo₃

inl.inl.inrh₁ ≤ h₂ → h₂ ≤ h₃ → sumo₁ < sumo₃
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: ¬sumo₂ = sumo₃

h✝: sumo₁ = sumo₃

inl.inr.inlh₁ ≤ h₂ → sumo₂ < sumo₃ → h₁ ≤ h₃
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: ¬sumo₂ = sumo₃

h✝: ¬sumo₁ = sumo₃

inl.inr.inrh₁ ≤ h₂ → sumo₂ < sumo₃ → sumo₁ < sumo₃
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: sumo₂ = sumo₃

h✝: sumo₁ = sumo₃

inr.inl.inlsumo₁ < sumo₂ → h₂ ≤ h₃ → h₁ ≤ h₃
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: sumo₂ = sumo₃

h✝: ¬sumo₁ = sumo₃

inr.inl.inrsumo₁ < sumo₂ → h₂ ≤ h₃ → sumo₁ < sumo₃
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: ¬sumo₂ = sumo₃

h✝: sumo₁ = sumo₃

inr.inr.inlsumo₁ < sumo₂ → sumo₂ < sumo₃ → h₁ ≤ h₃
sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: ¬sumo₂ = sumo₃

h✝: ¬sumo₁ = sumo₃

inr.inr.inrsumo₁ < sumo₂ → sumo₂ < sumo₃ → sumo₁ < sumo₃ 
      
∀ {c₁ c₂ c₃ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₃ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₁ c₃ =         truecase inl.inl.inl | inr.inr.inl | inr.inr.inr | inr.inl.inr => 
        sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: sumo₂ = sumo₃

h✝: ¬sumo₁ = sumo₃

sumo₁ < sumo₂ → h₂ ≤ h₃ → sumo₁ < sumo₃intro h1: sumo₁ < sumo₂
h1 h2: h₂ ≤ h₃
h2sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: ¬sumo₂ = sumo₃

h✝: sumo₁ = sumo₃

h1: sumo₁ < sumo₂

h2: sumo₂ < sumo₃

h₁ ≤ h₃ 
        sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: ¬sumo₁ = sumo₂

h✝¹: ¬sumo₂ = sumo₃

h✝: sumo₁ = sumo₃

sumo₁ < sumo₂ → sumo₂ < sumo₃ → h₁ ≤ h₃linarith
Goals accomplished! 🐙
      
∀ {c₁ c₂ c₃ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₃ =         true →
      (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₁ c₃ =         truecase inl.inl.inr | inl.inr.inl | inl.inr.inr | inr.inl.inl => 
        sumo₁, h₁, sumo₂, h₂, sumo₃, h₃: ℕ

h✝²: sumo₁ = sumo₂

h✝¹: ¬sumo₂ = sumo₃

h✝: sumo₁ = sumo₃

h₁ ≤ h₂ → sumo₂ < sumo₃ → h₁ ≤ h₃simp [*] at *
Goals accomplished! 🐙
    }
Goals accomplished! 🐙,
    le_antisymm := by
Goals accomplished! 🐙 
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂{
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂
      
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂intro ⟨sumo₁: ℕ
sumo₁, h₁: ℕ
h₁⟩ ⟨sumo₂: ℕ
sumo₂, h₂: ℕ
h₂⟩sumo₁, h₁, sumo₂, h₂: ℕ

(fun x x_1 =>
        match x with
        | (sumo₁, h₁) =>
          match x_1 with
          | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
      (sumo₁, h₁) (sumo₂, h₂) =     true →
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        (sumo₂, h₂) (sumo₁, h₁) =       true →
    (sumo₁, h₁) = (sumo₂, h₂)
      
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂simpsumo₁, h₁, sumo₂, h₂: ℕ

(if sumo₁ = sumo₂ then h₁ ≤ h₂ else sumo₁ < sumo₂) →
  (if sumo₂ = sumo₁ then h₂ ≤ h₁ else sumo₂ < sumo₁) → sumo₁ = sumo₂ ∧ h₁ = h₂
      
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂split_ifssumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: sumo₁ = sumo₂

h✝: sumo₂ = sumo₁

inl.inlh₁ ≤ h₂ → h₂ ≤ h₁ → sumo₁ = sumo₂ ∧ h₁ = h₂
sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

inl.inrh₁ ≤ h₂ → sumo₂ < sumo₁ → sumo₁ = sumo₂ ∧ h₁ = h₂
sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: sumo₂ = sumo₁

inr.inlsumo₁ < sumo₂ → h₂ ≤ h₁ → sumo₁ = sumo₂ ∧ h₁ = h₂
sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

inr.inrsumo₁ < sumo₂ → sumo₂ < sumo₁ → sumo₁ = sumo₂ ∧ h₁ = h₂
      
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂case inl.inl h: sumo₂ = sumo₁
h => 
        sumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h₁ ≤ h₂ → h₂ ≤ h₁ → sumo₁ = sumo₂ ∧ h₁ = h₂intro h1: h₁ ≤ h₂
h1 h2: h₂ ≤ h₁
h2sumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h1: h₁ ≤ h₂

h2: h₂ ≤ h₁

sumo₁ = sumo₂ ∧ h₁ = h₂ 
        sumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h₁ ≤ h₂ → h₂ ≤ h₁ → sumo₁ = sumo₂ ∧ h₁ = h₂simp [h: sumo₂ = sumo₁
h]sumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h1: h₁ ≤ h₂

h2: h₂ ≤ h₁

h₁ = h₂
        sumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h₁ ≤ h₂ → h₂ ≤ h₁ → sumo₁ = sumo₂ ∧ h₁ = h₂dwi { sumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h1: h₁ ≤ h₂

h2: h₂ ≤ h₁

h₁ = h₂apply Nat.le_antisymm: ∀ {n m : ℕ}, n ≤ m → m ≤ n → n = m
Nat.le_antisymmsumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h1: h₁ ≤ h₂

h2: h₂ ≤ h₁

h₁h₁ ≤ h₂
sumo₁, h₁, sumo₂, h₂: ℕ

h✝: sumo₁ = sumo₂

h: sumo₂ = sumo₁

h1: h₁ ≤ h₂

h2: h₂ ≤ h₁

h₂h₂ ≤ h₁ }
Goals accomplished! 🐙
      
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂case inl.inr | inr.inl => 
        sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: sumo₂ = sumo₁

sumo₁ < sumo₂ → h₂ ≤ h₁ → sumo₁ = sumo₂ ∧ h₁ = h₂simp [*] at *
Goals accomplished! 🐙
      
∀ {c₁ c₂ : ℕ × ℕ},
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true →
    (fun x x_1 =>
            match x with
            | (sumo₁, h₁) =>
              match x_1 with
              | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
          c₂ c₁ =         true →
      c₁ = c₂case inr.inr => 
        sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

sumo₁ < sumo₂ → sumo₂ < sumo₁ → sumo₁ = sumo₂ ∧ h₁ = h₂intro h1: sumo₁ < sumo₂
h1 h2: sumo₂ < sumo₁
h2sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

h1: sumo₁ < sumo₂

h2: sumo₂ < sumo₁

sumo₁ = sumo₂ ∧ h₁ = h₂ 
        sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

sumo₁ < sumo₂ → sumo₂ < sumo₁ → sumo₁ = sumo₂ ∧ h₁ = h₂linarith
Goals accomplished! 🐙
    }
Goals accomplished! 🐙
    le_total := by
Goals accomplished! 🐙 
∀ (c₁ c₂ : ℕ × ℕ),
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true ∨     (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₂ c₁ =       true{
∀ (c₁ c₂ : ℕ × ℕ),
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true ∨     (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₂ c₁ =       true
      
∀ (c₁ c₂ : ℕ × ℕ),
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true ∨     (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₂ c₁ =       trueintro ⟨sumo₁: ℕ
sumo₁, h₁: ℕ
h₁⟩ ⟨sumo₂: ℕ
sumo₂, h₂: ℕ
h₂⟩sumo₁, h₁, sumo₂, h₂: ℕ

(fun x x_1 =>
        match x with
        | (sumo₁, h₁) =>
          match x_1 with
          | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
      (sumo₁, h₁) (sumo₂, h₂) =     true ∨   (fun x x_1 =>
        match x with
        | (sumo₁, h₁) =>
          match x_1 with
          | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
      (sumo₂, h₂) (sumo₁, h₁) =     true
      
∀ (c₁ c₂ : ℕ × ℕ),
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true ∨     (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₂ c₁ =       truesimpsumo₁, h₁, sumo₂, h₂: ℕ

(if sumo₁ = sumo₂ then h₁ ≤ h₂ else sumo₁ < sumo₂) ∨ if sumo₂ = sumo₁ then h₂ ≤ h₁ else sumo₂ < sumo₁
      
∀ (c₁ c₂ : ℕ × ℕ),
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true ∨     (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₂ c₁ =       truesplit_ifssumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: sumo₁ = sumo₂

h✝: sumo₂ = sumo₁

inl.inlh₁ ≤ h₂ ∨ h₂ ≤ h₁
sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

inl.inrh₁ ≤ h₂ ∨ sumo₂ < sumo₁
sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: sumo₂ = sumo₁

inr.inlsumo₁ < sumo₂ ∨ h₂ ≤ h₁
sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

inr.inrsumo₁ < sumo₂ ∨ sumo₂ < sumo₁
      
∀ (c₁ c₂ : ℕ × ℕ),
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true ∨     (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₂ c₁ =       truecase inl.inl => sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: sumo₁ = sumo₂

h✝: sumo₂ = sumo₁

h₁ ≤ h₂ ∨ h₂ ≤ h₁apply Nat.le_total: ∀ (m n : ℕ), m ≤ n ∨ n ≤ m
Nat.le_total
Goals accomplished! 🐙
      
∀ (c₁ c₂ : ℕ × ℕ),
  (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₁ c₂ =       true ∨     (fun x x_1 =>
          match x with
          | (sumo₁, h₁) =>
            match x_1 with
            | (sumo₂, h₂) => if sumo₁ = sumo₂ then decide (h₁ ≤ h₂) else decide (sumo₁ < sumo₂))
        c₂ c₁ =       truecase inl.inr | inr.inl | inr.inr => sumo₁, h₁, sumo₂, h₂: ℕ

h✝¹: ¬sumo₁ = sumo₂

h✝: ¬sumo₂ = sumo₁

sumo₁ < sumo₂ ∨ sumo₂ < sumo₁simp [*] at *
Goals accomplished! 🐙
    }
Goals accomplished! 🐙
  }