diff options
| author | Andreas Grois <andi@grois.info> | 2023-12-18 22:03:15 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2023-12-18 22:03:15 +0100 |
| commit | e1f64e3a14366e3733fbfd5b5de4d120bb352c11 (patch) | |
| tree | 068f0905f6141803d92e351f207d2b7c736a6c7a /Common/Nat.lean | |
| parent | d99b0b2bddd3641b0acb58373f942c6beab8b03e (diff) | |
Even more cleanup in Heap
Diffstat (limited to 'Common/Nat.lean')
| -rw-r--r-- | Common/Nat.lean | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Common/Nat.lean b/Common/Nat.lean index fd7337b..5725b6c 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -151,3 +151,9 @@ theorem Nat.odd_not_even_odd {n : Nat} : Nat.isOdd n ↔ ¬Nat.isEven n := theorem Nat.even_not_odd_even {n : Nat} : Nat.isEven n ↔ ¬Nat.isOdd n := Iff.intro Nat.even_not_odd Nat.not_odd_even + +theorem Nat.pred_even_odd {n : Nat} (h₁ : Nat.isEven n) (h₂ : n > 0) : Nat.isOdd n.pred := by + cases n with + | zero => contradiction + | succ o => simp[Nat.isEven] at h₁ + assumption |