From c05a9435a06d3002da2d40f83ac7281ae198a64a Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 12 Feb 2024 23:27:35 +0900 Subject: [PATCH] feat: add lemmas about `Nat.add` --- Std/Data/Nat/Lemmas.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean index a0c16adb9d..2671e31804 100644 --- a/Std/Data/Nat/Lemmas.lean +++ b/Std/Data/Nat/Lemmas.lean @@ -194,6 +194,24 @@ protected def sum_trichotomy (a b : Nat) : a < b ⊕' a = b ⊕' b < a := @[deprecated] alias succ_add_eq_succ_add := Nat.succ_add_eq_add_succ +protected theorem add_left_eq_self {n m : Nat} : n + m = m ↔ n = 0 := by + conv => lhs; rhs; rw [← Nat.zero_add m] + rw [Nat.add_right_cancel_iff] + +protected theorem add_right_eq_self {n m : Nat} : n + m = n ↔ m = 0 := by + conv => lhs; rhs; rw [← Nat.add_zero n] + rw [Nat.add_left_cancel_iff] + +protected theorem add_left_le_self {n m : Nat} : n + m ≤ m ↔ n = 0 := by + conv => lhs; rhs; rw [← Nat.zero_add m] + rw [Nat.add_le_add_iff_right] + apply Nat.le_zero + +protected theorem add_right_le_self {n m : Nat} : n + m ≤ n ↔ m = 0 := by + conv => lhs; rhs; rw [← Nat.add_zero n] + rw [Nat.add_le_add_iff_left] + apply Nat.le_zero + /-! ## sub -/ @[deprecated] protected alias le_of_le_of_sub_le_sub_right := Nat.le_of_sub_le_sub_right