feat(algebra/group_power/basic): add add le_of_pow_le_pow (#5054)

add a random missing lemma
leanprover-community · Nov 20, 2020 · 006f84e · 006f84e
1 parent 1fbdf77
commit 006f84e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/algebra/group_power/basic.lean b/src/algebra/group_power/basic.lean
@@ -588,6 +588,9 @@ lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i :
 lemma lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
 lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
 
+lemma le_of_pow_le_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (hn : 0 < n) (h : a ^ n ≤ b ^ n) : a ≤ b :=
+le_of_not_lt $ λ h1, not_le_of_lt (pow_lt_pow_of_lt_left h1 hb hn) h
+
 end linear_ordered_semiring
 
 theorem pow_two_nonneg [linear_ordered_ring R] (a : R) : 0 ≤ a ^ 2 :=