diff --git a/tests/lean/grind/algebra/linarith_field.lean b/tests/lean/grind/algebra/linarith_field.lean new file mode 100644 index 0000000000..1ca8e581d1 --- /dev/null +++ b/tests/lean/grind/algebra/linarith_field.lean @@ -0,0 +1,14 @@ +open Lean.Grind + +variable {α : Type} [Field α] [LinearOrder α] [OrderedRing α] + +example (a b : α) (h : a < b / 2) : 2 * a < b := by grind +example (a b : α) (h : a < b / 2) : a + a < b := by grind +example (a b : α) (h : a < b / 2) : 2 * a ≤ b := by grind +example (a b : α) (h : a < b / 2) : a + a ≤ b := by grind +example (a b : α) (h : a ≤ b / 2) : 2 * a ≤ b := by grind +example (a b : α) (h : a ≤ b / 2) : a + a ≤ b := by grind + +example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind + +example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind