We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent ad7d44e commit 142df23Copy full SHA for 142df23
src/Init/Grind/Ordered/Ring.lean
@@ -154,8 +154,6 @@ theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) :
154
theorem natCast_nonneg {a : Nat} : 0 ≤ (a : R) := by
155
simpa [Semiring.natCast_zero] using natCast_le_natCast_of_le (R := R) _ _ (Nat.zero_le a)
156
157
-grind_pattern natCast_nonneg => (a : R)
158
-
159
theorem natCast_lt_natCast_of_lt (a b : Nat) : a < b → (a : R) < (b : R) := by
160
induction a generalizing b <;> cases b <;> simp
161
next n =>
0 commit comments