feat(data/nat/basic): le_of_add_le_* (#6145)

leanprover-community · Feb 10, 2021 · 14a1fd7 · 14a1fd7
1 parent dbbac3b
commit 14a1fd7
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
@@ -344,6 +344,13 @@ begin
   exact add_lt_add_of_lt_of_le hab (nat.succ_le_iff.2 hcd)
 end
 
+-- TODO: generalize to some ordered add_monoids, based on #6145
+lemma le_of_add_le_left {a b c : ℕ} (h : a + b ≤ c) : a ≤ c :=
+by { refine le_trans _ h, simp }
+
+lemma le_of_add_le_right {a b c : ℕ} (h : a + b ≤ c) : b ≤ c :=
+by { refine le_trans _ h, simp }
+
 /-! ### `pred` -/
 
 @[simp]

diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
@@ -325,6 +325,13 @@ begin
   exact h _ ((lt_add_iff_pos_right b).1 hxb)
 end
 
+-- TODO: generalize to some ordered add_monoids, based on #6145
+lemma le_of_add_le_left {a b c : ℝ≥0} (h : a + b ≤ c) : a ≤ c :=
+by { refine le_trans _ h, simp }
+
+lemma le_of_add_le_right {a b c : ℝ≥0} (h : a + b ≤ c) : b ≤ c :=
+by { refine le_trans _ h, simp }
+
 lemma lt_iff_exists_rat_btwn (a b : ℝ≥0) :
   a < b ↔ (∃q:ℚ, 0 ≤ q ∧ a < nnreal.of_real q ∧ nnreal.of_real q < b) :=
 iff.intro