diff options
| author | Andreas Grois <andi@grois.info> | 2024-06-30 20:58:59 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-06-30 20:58:59 +0200 |
| commit | 97e8285eaaacf54fd3689fc2862a1faea81694dd (patch) | |
| tree | 7b79a9bb3535d771bb90e3b666ba31242946cc74 /Common/Nat.lean | |
| parent | cf1bc3567a2111f11eb45923d03d1e1ef3c01c52 (diff) | |
Finish CompleteTree.get implementation. Not proven to be correct yet.
Diffstat (limited to 'Common/Nat.lean')
| -rw-r--r-- | Common/Nat.lean | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Common/Nat.lean b/Common/Nat.lean index 1721653..0a0f1f4 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -166,3 +166,11 @@ theorem Nat.sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) : have h₇ : 1 + (a-b) ≤ c := h₆.subst (motive := λx ↦ x ≤ c) h₅ have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇ Nat.lt_of_succ_le h₈ + +theorem Nat.sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a - b < c - b) := by + apply Nat.sub_lt_of_lt_add + case h₂ => assumption + case h₁ => + have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂ + rw[Nat.sub_add_cancel h₃] + assumption |