induction n using Nat.case_strong_induction_on with
| hi n₀ ih =>
  intro a hsz
  apply le_trans (splitTimeCost _ _)
  apply le_of_eq_of_le
  apply Eq.trans
  apply Nat.add_right_comm _ _ _
  apply Nat.add_comm
  apply add_le_add _
  apply hsi
  apply le_trans
  apply Trace.CostedProgram.recurseTimeCostBound (x := x * n₀ + x)
  intro arg harg
  apply le_trans _ (add_le_add_right (mul_le_mul (le_refl _ ) _ (zero_le _) (zero_le _)) _)
  use sz arg
  specialize ih (sz arg) _
  apply Nat.succ_le_succ_iff.mp
  apply le_of_le_of_eq _ hsz
  apply Nat.succ_le_of_lt harg
  specialize ih _ rfl
  simp only [p.costedMatches']
  apply ih
  apply Nat.succ_le_succ_iff.mp
  apply le_of_le_of_eq _ hsz
  apply Nat.succ_le_of_lt harg
  simp only [p.costedMatches, hr, one_mul, Nat.mul_succ]
  apply le_refl
| hz =>
  intro a hsz
  apply le_trans (splitTimeCost _ _)
  apply le_of_eq_of_le
  apply Eq.trans
  apply Nat.add_right_comm _ _ _
  apply Nat.add_comm
  apply add_le_add _
  apply hsi
  apply le_of_eq_of_le _ (zero_le _)
  apply Trace.CostedProgram.recurseTimeCost_leaf (costed_sound h) _ hsz
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 : ℕ
⊢ ∀ (a : α), sz a = n → timeCost' p h a ≤ x * n + x
no goals