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

State before:
n : ℕ
npos : 0 < n
⊢ 2 * (n - 1) + 1 = 2 * n - 1
Tactic:
cases' n with n
State after:
case zero
npos : 0 < 0
⊢ 2 * (0 - 1) + 1 = 2 * 0 - 1

case succ
n : ℕ
npos : 0 < n + 1
⊢ 2 * (n + 1 - 1) + 1 = 2 * (n + 1) - 1

State before:
case zero
npos : 0 < 0
⊢ 2 * (0 - 1) + 1 = 2 * 0 - 1
Tactic:
exact (lt_asymm npos npos).elim
State after:
no goals

State before:
case succ
n : ℕ
npos : 0 < n + 1
⊢ 2 * (n + 1 - 1) + 1 = 2 * (n + 1) - 1
Tactic:
rfl
State after:
no goals