feat(algebra/archimedean): pow_unbounded_of_gt_one (#50)

algebra/archimedean.lean

@@ -107,6 +107,14 @@ let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
 section linear_ordered_ring
 variables [linear_ordered_ring α] [archimedean α]
 
+lemma pow_unbounded_of_gt_one (x : α) {y : α} 
+    (hy1 : 1 < y) : ∃ n : ℕ, x < monoid.pow y n :=
+have hy0 : 0 <  y - 1 := sub_pos_of_lt hy1,
+let ⟨n, h⟩ := archimedean.arch x hy0 in
+⟨n, calc x ≤ (y - 1) • n     : h
+       ... < 1 + (y - 1) • n : by rw add_comm; exact lt_add_one _
+       ... ≤ monoid.pow y n  : pow_ge_one_add_sub_mul (le_of_lt hy1) _⟩
+
 theorem exists_int_gt (x : α) : ∃ n : ℤ, x < n :=
 let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by simp [h]⟩