Theorem: Poland1998P4.a_recurrence (Compfiles/Poland1998P4.lean)

State before:
n : ℕ
hn : 2 ≤ n
⊢ a n = a (n - 1) + a (n / 2)
Tactic:
cases' n with n
State after:
case zero
hn : 2 ≤ 0
⊢ a 0 = a (0 - 1) + a (0 / 2)

case succ
n : ℕ
hn : 2 ≤ n + 1
⊢ a (n + 1) = a (n + 1 - 1) + a ((n + 1) / 2)

State before:
case zero
hn : 2 ≤ 0
⊢ a 0 = a (0 - 1) + a (0 / 2)
Tactic:
exact (Nat.not_succ_le_zero _ hn).elim
State after:
no goals

State before:
case succ
n : ℕ
hn : 2 ≤ n + 1
⊢ a (n + 1) = a (n + 1 - 1) + a ((n + 1) / 2)
Tactic:
cases' n
State after:
case succ.zero
hn : 2 ≤ 0 + 1
⊢ a (0 + 1) = a (0 + 1 - 1) + a ((0 + 1) / 2)

case succ.succ
n✝ : ℕ
hn : 2 ≤ n✝ + 1 + 1
⊢ a (n✝ + 1 + 1) = a (n✝ + 1 + 1 - 1) + a ((n✝ + 1 + 1) / 2)

State before:
case succ.zero
hn : 2 ≤ 0 + 1
⊢ a (0 + 1) = a (0 + 1 - 1) + a ((0 + 1) / 2)
Tactic:
exact (Nat.not_succ_le_self _ hn).elim
State after:
no goals

State before:
case succ.succ
n✝ : ℕ
hn : 2 ≤ n✝ + 1 + 1
⊢ a (n✝ + 1 + 1) = a (n✝ + 1 + 1 - 1) + a ((n✝ + 1 + 1) / 2)
Tactic:
simp only [a, Nat.succ_sub_succ_eq_sub, tsub_zero]
State after:
no goals