Lemmas about densely linearly ordered groups.

theorem le_of_forall_lt_one_mul_le {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b : α} (h : ∀ ε < 1, a * ε ≤ b) : a ≤ b

theorem le_of_forall_neg_add_le {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b : α} (h : ∀ ε < 0, a + ε ≤ b) : a ≤ b

theorem le_of_forall_one_lt_div_le {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b : α} (h : ∀ (ε : α), 1 < ε → a / ε ≤ b) : a ≤ b

theorem le_of_forall_pos_sub_le {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b : α} (h : ∀ (ε : α), 0 < ε → a - ε ≤ b) : a ≤ b

theorem le_iff_forall_lt_one_mul_le {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b : α} : a ≤ b ↔ ∀ ε < 1, a * ε ≤ b

theorem le_iff_forall_neg_add_le {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b : α} : a ≤ b ↔ ∀ ε < 0, a + ε ≤ b

theorem le_mul_of_forall_lt {α : Type u_1} [CommGroup α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

theorem le_add_of_forall_lt {α : Type u_1} [AddCommGroup α] [LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') : c ≤ a + b

theorem mul_le_of_forall_lt {α : Type u_1} [CommGroup α] [LinearOrder α] [MulLeftMono α] [DenselyOrdered α] {a b c : α} (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) : a * b ≤ c

theorem add_le_of_forall_lt {α : Type u_1} [AddCommGroup α] [LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b c : α} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c

theorem exists_pow_lt_of_one_lt {M : Type u_2} [LinearOrder M] [DenselyOrdered M] {x : M} [CommMonoid M] [ExistsMulOfLE M] [IsOrderedCancelMonoid M] (hx : 1 < x) (n : ℕ) : ∃ (y : M), 1 < y ∧ y ^ n < x

theorem exists_nsmul_lt_of_pos {M : Type u_2} [LinearOrder M] [DenselyOrdered M] {x : M} [AddCommMonoid M] [ExistsAddOfLE M] [IsOrderedCancelAddMonoid M] (hx : 0 < x) (n : ℕ) : ∃ (y : M), 0 < y ∧ n • y < x

theorem exists_lt_pow_of_lt_one {M : Type u_2} [LinearOrder M] [DenselyOrdered M] {x : M} [CommGroup M] [IsOrderedCancelMonoid M] (hx : x < 1) (n : ℕ) : ∃ y < 1, x < y ^ n

theorem exists_lt_nsmul_of_neg {M : Type u_2} [LinearOrder M] [DenselyOrdered M] {x : M} [AddCommGroup M] [IsOrderedCancelAddMonoid M] (hx : x < 0) (n : ℕ) : ∃ y < 0, x < n • y