Compare commits

...

2 Commits

Author SHA1 Message Date
Kim Morrison
142df231dd remove grind_pattern, it fires too much, we'll need to do this internally 2025-12-11 09:24:35 +11:00
Kim Morrison
ad7d44e201 feat: grind_pattern natCast_nonneg 2025-12-10 16:19:55 +11:00

View File

@@ -151,6 +151,9 @@ theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) :
simp [Semiring.natCast_add, Semiring.natCast_one]
exact OrderedAdd.add_le_left_iff _ |>.mp ih
theorem natCast_nonneg {a : Nat} : 0 (a : R) := by
simpa [Semiring.natCast_zero] using natCast_le_natCast_of_le (R := R) _ _ (Nat.zero_le a)
theorem natCast_lt_natCast_of_lt (a b : Nat) : a < b (a : R) < (b : R) := by
induction a generalizing b <;> cases b <;> simp
next n =>