From 775f27f47861641561ea8fe4dc8b9ce1e48a47f9 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Wed, 10 Jul 2024 09:20:13 +0200
Subject: Continue on CompleteTree.heapReplaceElementAtIsHeap

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

(limited to 'Common/Nat.lean')

diff --git a/Common/Nat.lean b/Common/Nat.lean
index 0a0f1f4..9d4d538 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -174,3 +174,10 @@ theorem Nat.sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a
     have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂
     rw[Nat.sub_add_cancel h₃]
     assumption
+
+theorem Nat.add_eq_zero {a b : Nat} :  a + b = 0 ↔ a = 0 ∧ b = 0 := by
+  constructor <;> intro h₁
+  case mpr =>
+    simp[h₁]
+  case mp =>
+    cases a <;> simp_arith at *; assumption
-- 
cgit v1.2.3

