Skip to content

Commit 5be60e5

Browse files
committed
fix: cheaper test first
1 parent b5074f0 commit 5be60e5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Init/Data/Nat/Div/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -180,8 +180,8 @@ theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
180180
(mod_eq a b).symm ▸ this
181181

182182
grind_pattern mod_eq_of_lt => a % b where
183-
guard a < b
184183
not_value b
184+
guard a < b
185185

186186
@[simp] theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1 := by
187187
match n with

0 commit comments

Comments
 (0)