Theorem: Misc.Nat.odd_pred_of_even (LeanSAT/Util/Misc.lean)

State before:
n : Nat
h : n > 0
⊢ Even n → Odd (n - 1)
Tactic:
intro
State after:
n : Nat
h : n > 0
a✝ : Even n
⊢ Odd (n - 1)

State before:
n : Nat
h : n > 0
a✝ : Even n
⊢ Odd (n - 1)
Tactic:
apply Classical.byContradiction
State after:
case h
n : Nat
h : n > 0
a✝ : Even n
⊢ ¬Odd (n - 1) → False

State before:
case h
n : Nat
h : n > 0
a✝ : Even n
⊢ ¬Odd (n - 1) → False
Tactic:
intro h'
State after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
⊢ False
Tactic:
have := Iff.mp Nat.not_odd_iff_even h'
State after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this : Even (n - 1)
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this : Even (n - 1)
⊢ False
Tactic:
have : Odd (n - 1 + 1) := Nat.odd_succ_of_even this
State after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd (n - 1 + 1)
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd (n - 1 + 1)
⊢ False
Tactic:
rw [Nat.sub_add_cancel h] at this
State after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd n
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝ : Even (n - 1)
this : Odd n
⊢ False
Tactic:
have := Iff.mp Nat.odd_iff_not_even this
State after:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝¹ : Even (n - 1)
this✝ : Odd n
this : ¬Even n
⊢ False

State before:
case h
n : Nat
h : n > 0
a✝ : Even n
h' : ¬Odd (n - 1)
this✝¹ : Even (n - 1)
this✝ : Odd n
this : ¬Even n
⊢ False
Tactic:
contradiction
State after:
no goals