ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a + b < c<VAR>hle : d ≤ a<GOAL>d + b < c
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a * b < c<VAR>hle : d ≤ a<GOAL>d * b < c
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a * b ≤ c<VAR>hle : d ≤ a<GOAL>d * b ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a + b ≤ c<VAR>hle : d ≤ a<GOAL>d + b ≤ c
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a < b + c<VAR>hle : c ≤ d<GOAL>a < b + d
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a < b * c<VAR>hle : c ≤ d<GOAL>a < b * d
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a ≤ b * c<VAR>hle : c ≤ d<GOAL>a ≤ b * d
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a ≤ b + c<VAR>hle : c ≤ d<GOAL>a ≤ b + d
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a < b + c<VAR>hle : b ≤ d<GOAL>a < d + c
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a < b * c<VAR>hle : b ≤ d<GOAL>a < d * c
<VAR>α : Type u_1<VAR>Mul α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a ≤ b * c<VAR>hle : b ≤ d<GOAL>a ≤ d * c
<VAR>α : Type u_1<VAR>Add α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>h : a ≤ b + c<VAR>hle : b ≤ d<GOAL>a ≤ d + c
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a + b = a + c<GOAL>b = c
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a * b = a * c<GOAL>b = c
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a + b = c + b<GOAL>a = c
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : a * b = c * b<GOAL>a = c
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<GOAL>a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<GOAL>a₂ + b₂ ≤ a₁ + b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>Mul α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<VAR>hac : a ≤ c<VAR>hbd : b ≤ d<GOAL>a * b = c * d ↔ a = c ∧ b = d
<VAR>α : Type u_1<VAR>Add α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c d : α<VAR>hac : a ≤ c<VAR>hbd : b ≤ d<GOAL>a + b = c + d ↔ a = c ∧ b = d
<VAR>α : Type u_1<VAR>Add α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a + b < c + d<GOAL>min a b < max c d
<VAR>α : Type u_1<VAR>Mul α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a * b < c * d<GOAL>min a b < max c d
<VAR>α : Type u_1<VAR>Mul α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a * b ≤ c * d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>Add α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a + b ≤ c + d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>Mul α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>h : a * b ≤ c * d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>Add α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : a + b ≤ c + d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>Mul α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>h : a * b ≤ c * d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>Add α<VAR>LinearOrder α<VAR>a b c d : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : a + b ≤ c + d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>Mul α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>max (a * b) (c * d) ≤ max a c * max b d
<VAR>α : Type u_1<VAR>Add α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>max (a + b) (c + d) ≤ max a c + max b d
<VAR>α : Type u_1<VAR>Add α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>min a c + min b d ≤ min (a + b) (c + d)
<VAR>α : Type u_1<VAR>Mul α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>min a c * min b d ≤ min (a * b) (c * d)
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : 1 ≤ b<GOAL>a ≤ a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : 0 ≤ b<GOAL>a ≤ a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ 1<GOAL>a * b ≤ a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ 0<GOAL>a + b ≤ a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : 0 ≤ b<GOAL>a ≤ b + a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : 1 ≤ b<GOAL>a ≤ b * a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ 1<GOAL>b * a ≤ a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ 0<GOAL>b + a ≤ a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a ≤ a * b<GOAL>1 ≤ b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a ≤ a + b<GOAL>0 ≤ b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a + b ≤ a<GOAL>b ≤ 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a * b ≤ a<GOAL>b ≤ 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ a + b<GOAL>0 ≤ a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ a * b<GOAL>1 ≤ a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a * b ≤ b<GOAL>a ≤ 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a + b ≤ b<GOAL>a ≤ 0
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a ≤ a + b ↔ 0 ≤ b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a ≤ a * b ↔ 1 ≤ b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a ≤ b * a ↔ 1 ≤ b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a ≤ b + a ↔ 0 ≤ b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a * b ≤ a ↔ b ≤ 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>b : α<GOAL>a + b ≤ a ↔ b ≤ 0
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a + b ≤ b ↔ a ≤ 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a * b ≤ b ↔ a ≤ 1
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : 1 < b<GOAL>a < a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : 0 < b<GOAL>a < a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : b < 1<GOAL>a * b < a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : b < 0<GOAL>a + b < a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : 0 < b<GOAL>a < b + a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : 1 < b<GOAL>a < b * a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : b < 0<GOAL>b + a < a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<VAR>h : b < 1<GOAL>b * a < a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < a + b<GOAL>0 < b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < a * b<GOAL>1 < b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a + b < a<GOAL>b < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a * b < a<GOAL>b < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : b < a + b<GOAL>0 < a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : b < a * b<GOAL>1 < a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a * b < b<GOAL>a < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a + b < b<GOAL>a < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a < a * b ↔ 1 < b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a < a + b ↔ 0 < b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a < b + a ↔ 0 < b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a < b * a ↔ 1 < b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a + b < a ↔ b < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a * b < a ↔ b < 1
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a * b < b ↔ a < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>LT α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>b : α<GOAL>a + b < b ↔ a < 0
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : a ≤ 0<GOAL>b + a ≤ c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : a ≤ 1<GOAL>b * a ≤ c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : a < 0<GOAL>b + a < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : a < 1<GOAL>b * a < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : a ≤ 1<GOAL>b * a < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : a ≤ 0<GOAL>b + a < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : a < 0<GOAL>b + a < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : a < 1<GOAL>b * a < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : a < 0<GOAL>b + a < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : a < 1<GOAL>b * a < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>a + b ≤ 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<GOAL>a * b ≤ 1
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a ≤ 1<VAR>hb : b < 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a ≤ 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b ≤ 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a < 1<VAR>hb : b ≤ 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < 1<VAR>hb : b < 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a + b < 0
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : a < 1<VAR>hb : b < 1<GOAL>a * b < 1
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : 0 ≤ a<GOAL>b ≤ c + a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : 1 ≤ a<GOAL>b ≤ c * a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : 1 < a<GOAL>b < c * a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b ≤ c<VAR>ha : 0 < a<GOAL>b < c + a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : 1 ≤ a<GOAL>b < c * a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : 0 ≤ a<GOAL>b < c + a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : 0 < a<GOAL>b < c + a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : 1 < a<GOAL>b < c * a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : 1 < a<GOAL>b < c * a
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>hbc : b < c<VAR>ha : 0 < a<GOAL>b < c + a
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>1 ≤ a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>0 ≤ a + b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 1 ≤ a<VAR>hb : 1 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 ≤ b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 < a<VAR>hb : 1 ≤ b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : 1 < a<VAR>hb : 1 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 1 < a<VAR>hb : 1 < b<GOAL>1 < a * b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : a ≤ 0<VAR>hbc : b ≤ c<GOAL>a + b ≤ c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : a ≤ 1<VAR>hbc : b ≤ c<GOAL>a * b ≤ c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : a < 0<VAR>hbc : b ≤ c<GOAL>a + b < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<VAR>ha : a < 1<VAR>hbc : b ≤ c<GOAL>a * b < c
<VAR>α : Type u_1<VAR>AddZeroClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : a ≤ 0<VAR>hb : b < c<GOAL>a + b < c
<VAR>α : Type u_1<VAR>MulOneClass α<VAR>Preorder α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>ha : a ≤ 1<VAR>hb : b < c<GOAL>a * b < c