diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean index 144a53e9eaec85..dc4d685401bbf0 100644 --- a/Mathlib/Data/Int/ModEq.lean +++ b/Mathlib/Data/Int/ModEq.lean @@ -251,6 +251,10 @@ theorem dvd_iff (h : a ≡ b [ZMOD n]) : n ∣ a ↔ n ∣ b := by end ModEq +@[simp] +theorem modEq_two_abs : |a| ≡ a [ZMOD 2] := by + grind [Int.ModEq] + @[simp] theorem modulus_modEq_zero : n ≡ 0 [ZMOD n] := by simp [ModEq]