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' > a → ∀ (b' : α), 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' > a → ∀ (b' : α), 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' < a → ∀ (b' : α), 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' < a → ∀ (b' : α), 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 : M), 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 : M), y < 0 ∧ x < n • y