apply Nat.succ_le_succ_iff.mp
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ sz arg ≤ n₀

case a
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ Nat.succ (sz arg) ≤ Nat.succ n₀

case a
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀