diff options
| author | Andreas Grois <andi@grois.info> | 2024-11-25 17:01:18 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-11-25 17:01:18 +0100 |
| commit | de5352e64f36948fc568a1bbb58bf930ec44aa2c (patch) | |
| tree | 227af0256b3ac725daa2911df104421286b8f691 /Common/Nat.lean | |
| parent | ce7214e07a766bc1e5ab02346e42eb6ca441c509 (diff) | |
Day 13, Part 1
Diffstat (limited to 'Common/Nat.lean')
| -rw-r--r-- | Common/Nat.lean | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Common/Nat.lean b/Common/Nat.lean index a863a49..3a605a9 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -15,3 +15,8 @@ theorem two_d_coordinate_to_index_lt_size {x y w h: Nat} (h₁ : x < w) (h₂ : theorem gt_of_sub_lt {a b c : Nat} (h₁ : a - b < a - c) : c < b := by omega theorem sub_lt_of_gt {a b c : Nat} (h₁ : b ≤ a) (h₂ : c < b) : a - b < a - c := by omega + +theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) := + match b with + | 0 => h₁ + | _ + 1 => /-(Nat.pred_succ a).substr $-/ Nat.lt_succ_of_lt h₁ |