diff options
| author | Andreas Grois <andi@grois.info> | 2024-07-10 09:20:13 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-07-10 09:20:13 +0200 |
| commit | 775f27f47861641561ea8fe4dc8b9ce1e48a47f9 (patch) | |
| tree | c00db8eab3fcf6289a04c9f930aed703ba4b6e5f /Common/Nat.lean | |
| parent | 97e8285eaaacf54fd3689fc2862a1faea81694dd (diff) | |
Continue on CompleteTree.heapReplaceElementAtIsHeap
Diffstat (limited to 'Common/Nat.lean')
| -rw-r--r-- | Common/Nat.lean | 7 |
1 files changed, 7 insertions, 0 deletions
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 |