feat(algebra/group_power/order): add pow_lt_self_of_lt_one (#17162)

leanprover-community · Oct 26, 2022 · 5118ae3 · 5118ae3
1 parent 5155be4
commit 5118ae3
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean
@@ -294,6 +294,10 @@ lemma pow_lt_pow_iff_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔
 lemma pow_lt_pow_of_lt_one (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
 (pow_lt_pow_iff_of_lt_one h ha).2 hij
 
+lemma pow_lt_self_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a :=
+calc a ^ n < a ^ 1 : pow_lt_pow_of_lt_one h₀ h₁ hn
+... = a : pow_one _
+
 lemma sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := by { rw sq, exact mul_pos ha ha }
 
 end strict_ordered_semiring