# Lemmas about densely linearly ordered groups. #

theorem le_of_forall_neg_add_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} (h : ∀ (ε : α), ε < 0a + ε b) :
a b
theorem le_of_forall_lt_one_mul_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} (h : ∀ (ε : α), ε < 1a * ε b) :
a b
theorem le_of_forall_pos_sub_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa - ε b) :
a b
theorem le_of_forall_one_lt_div_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa / ε b) :
a b
theorem le_iff_forall_pos_le_add {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} :
a b ∀ (ε : α), 0 < εa b + ε
theorem le_iff_forall_one_lt_le_mul {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} :
a b ∀ (ε : α), 1 < εa b * ε
theorem le_iff_forall_neg_add_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} :
a b ∀ (ε : α), ε < 0a + ε b
theorem le_iff_forall_lt_one_mul_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [] {a : α} {b : α} :
a b ∀ (ε : α), ε < 1a * ε b