diff options
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₁ |