Lemmas about densely linearly ordered groups.

theorem le_of_forall_neg_add_le {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), ε < 0 → a + ε ≤ b) : a ≤ b

theorem le_of_forall_lt_one_mul_le {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), ε < 1 → a * ε ≤ b) : a ≤ b

theorem le_of_forall_pos_sub_le {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), 0 < ε → a - ε ≤ b) : a ≤ b

theorem le_of_forall_one_lt_div_le {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} (h : ∀ (ε : α), 1 < ε → a / ε ≤ b) : a ≤ b

theorem le_iff_forall_pos_le_add {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 0 < ε → a ≤ b + ε

theorem le_iff_forall_one_lt_le_mul {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε

theorem le_iff_forall_neg_add_le {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), ε < 0 → a + ε ≤ b

theorem le_iff_forall_lt_one_mul_le {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [DenselyOrdered α] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), ε < 1 → a * ε ≤ b