From e1f64e3a14366e3733fbfd5b5de4d120bb352c11 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Mon, 18 Dec 2023 22:03:15 +0100
Subject: Even more cleanup in Heap

---
 Common/Nat.lean | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Common/Nat.lean')

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
-- 
cgit v1.2.3