Theorem: LoVe.Odd_3 (LoVe/Labs/Lab5Solution.lean)

State before:
⊢ Odd 3
Tactic:
intro ho3
State after:
ho3 : Even 3
⊢ False

State before:
ho3 : Even 3
⊢ False
Tactic:
cases ho3 with
| add_two _ ho1 =>
  cases ho1
State after:
no goals

State before:
case add_two
ho1 : Even 1
⊢ False
Tactic:
cases ho1
State after:
no goals