diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index 3b45978444a74..62732d1f94a16 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Joey van Langen, Casper Putz
 
 ! This file was ported from Lean 3 source module algebra.char_p.basic
-! leanprover-community/mathlib commit ceb887ddf3344dab425292e497fa2af91498437c
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -141,10 +141,16 @@ theorem CharP.int_cast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a
     rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
 #align char_p.int_cast_eq_zero_iff CharP.int_cast_eq_zero_iff
 
-theorem CharP.int_cast_eq_int_cast_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a b : ℤ) :
-    (a : R) = (b : R) ↔ a ≡ b [ZMOD p] := by
+theorem CharP.intCast_eq_intCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℤ} :
+    (a : R) = b ↔ a ≡ b [ZMOD p] := by
   rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
-#align char_p.int_coe_eq_int_coe_iff CharP.int_cast_eq_int_cast_iff
+#align char_p.int_cast_eq_int_cast CharP.intCast_eq_intCast
+
+theorem CharP.natCast_eq_natCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} :
+    (a : R) = b ↔ a ≡ b [MOD p] := by
+  rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
+  exact (CharP.intCast_eq_intCast _ _).trans Int.coe_nat_modEq_iff
+#align char_p.nat_cast_eq_nat_cast CharP.natCast_eq_natCast
 
 theorem CharP.eq [AddMonoidWithOne R] {p q : ℕ} (_c1 : CharP R p) (_c2 : CharP R q) : p = q :=
   Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R p q).1 (CharP.cast_eq_zero _ _))
@@ -286,10 +292,6 @@ theorem sub_pow_char_pow [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] {n :
   sub_pow_char_pow_of_commute _ _ _ (Commute.all _ _)
 #align sub_pow_char_pow sub_pow_char_pow
 
-theorem eq_iff_modEq_int [Ring R] (p : ℕ) [CharP R p] (a b : ℤ) : (a : R) = b ↔ a ≡ b [ZMOD p] := by
-  rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
-#align eq_iff_modeq_int eq_iff_modEq_int
-
 theorem CharP.neg_one_ne_one [Ring R] (p : ℕ) [CharP R p] [Fact (2 < p)] : (-1 : R) ≠ (1 : R) := by
   suffices (2 : R) ≠ 0 by
     intro h
diff --git a/Mathlib/Algebra/Ring/Divisibility.lean b/Mathlib/Algebra/Ring/Divisibility.lean
index 08a4bd5bf1505..d90aad4077e5c 100644
--- a/Mathlib/Algebra/Ring/Divisibility.lean
+++ b/Mathlib/Algebra/Ring/Divisibility.lean
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Ne
 Ported by: Matej Penciak
 
 ! This file was ported from Lean 3 source module algebra.ring.divisibility
-! leanprover-community/mathlib commit f1a2caaf51ef593799107fe9a8d5e411599f3996
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -125,6 +125,10 @@ theorem dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ b - c) : a ∣ b ↔ a 
     exact eq_add_of_sub_eq rfl
 #align dvd_iff_dvd_of_dvd_sub dvd_iff_dvd_of_dvd_sub
 
+--porting note: Needed to give an explicit argument to `dvd_neg`
+theorem dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [← dvd_neg a, neg_sub]
+#align dvd_sub_comm dvd_sub_comm
+
 end NonUnitalRing
 
 section Ring
diff --git a/Mathlib/Data/Int/GCD.lean b/Mathlib/Data/Int/GCD.lean
index cd27eae7d5703..9c9fb3cd076a1 100644
--- a/Mathlib/Data/Int/GCD.lean
+++ b/Mathlib/Data/Int/GCD.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sangwoo Jo (aka Jason), Guy Leroy, Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.int.gcd
-! leanprover-community/mathlib commit d4f69d96f3532729da8ebb763f4bc26fcf640f06
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -306,13 +306,13 @@ theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * natAbs j :
   apply Nat.gcd_mul_right
 #align int.gcd_mul_right Int.gcd_mul_right
 
-theorem gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_left (natAbs j) (natAbs_pos.2 i_non_zero)
-#align int.gcd_pos_of_non_zero_left Int.gcd_pos_of_non_zero_left
+theorem gcd_pos_of_ne_zero_left {i : ℤ} (j : ℤ) (hi : i ≠ 0) : 0 < gcd i j :=
+  Nat.gcd_pos_of_pos_left _ $ natAbs_pos.2 hi
+#align int.gcd_pos_of_ne_zero_left Int.gcd_pos_of_ne_zero_left
 
-theorem gcd_pos_of_non_zero_right (i : ℤ) {j : ℤ} (j_non_zero : j ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_right (natAbs i) (natAbs_pos.2 j_non_zero)
-#align int.gcd_pos_of_non_zero_right Int.gcd_pos_of_non_zero_right
+theorem gcd_pos_of_ne_zero_right (i : ℤ) {j : ℤ} (hj : j ≠ 0) : 0 < gcd i j :=
+  Nat.gcd_pos_of_pos_right _ $ natAbs_pos.2 hj
+#align int.gcd_pos_of_ne_zero_right Int.gcd_pos_of_ne_zero_right
 
 theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := by
   rw [gcd, Nat.gcd_eq_zero_iff, natAbs_eq_zero, natAbs_eq_zero]
@@ -430,7 +430,7 @@ theorem gcd_least_linear {a b : ℤ} (ha : a ≠ 0) :
     IsLeast { n : ℕ | 0 < n ∧ ∃ x y : ℤ, ↑n = a * x + b * y } (a.gcd b) := by
   simp_rw [← gcd_dvd_iff]
   constructor
-  · simpa [and_true_iff, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_non_zero_left b ha
+  · simpa [and_true_iff, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha
   · simp only [lowerBounds, and_imp, Set.mem_setOf_eq]
     exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn
 #align int.gcd_least_linear Int.gcd_least_linear
diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index b755f7c6e6820..257b3ff4b92d8 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module data.int.modeq
-! leanprover-community/mathlib commit 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -69,8 +69,14 @@ protected theorem trans : a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMO
 instance : IsTrans ℤ (ModEq n) where
   trans := @Int.ModEq.trans n
 
+protected theorem eq : a ≡ b [ZMOD n] → a % n = b % n := id
+#align int.modeq.eq Int.ModEq.eq
+
 end ModEq
 
+theorem modEq_comm : a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n] := ⟨ModEq.symm, ModEq.symm⟩
+#align int.modeq_comm Int.modEq_comm
+
 theorem coe_nat_modEq_iff {a b n : ℕ} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n] := by
   unfold ModEq Nat.ModEq; rw [← Int.ofNat_inj]; simp [coe_nat_mod]
 #align int.coe_nat_modeq_iff Int.coe_nat_modEq_iff
@@ -106,23 +112,32 @@ theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
   emod_emod _ _
 #align int.mod_modeq Int.mod_modEq
 
+@[simp]
+theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by
+--porting note: Restore old proof once #3309 is through
+  simp [-sub_neg_eq_add, neg_sub_neg, modEq_iff_dvd, dvd_sub_comm]
+#align int.neg_modeq_neg Int.neg_modEq_neg
+
+@[simp]
+theorem modEq_neg : a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n] := by simp [modEq_iff_dvd]
+#align int.modeq_neg Int.modEq_neg
+
 namespace ModEq
 
 protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m] :=
   modEq_iff_dvd.2 <| d.trans h.dvd
 #align int.modeq.of_dvd Int.ModEq.of_dvd
 
-protected theorem mul_left' (hc : 0 ≤ c) (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=
-  match hc.lt_or_eq with
-  | .inl hc => by
-    unfold ModEq
-    simp [mul_emod_mul_of_pos _ _ hc, show _ = _ from h]
-  | .inr hc => by
-    simp [hc.symm]
+protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] := by
+  obtain hc | rfl | hc := lt_trichotomy c 0
+  · rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
+    simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
+  · simp
+  · simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]
 #align int.modeq.mul_left' Int.ModEq.mul_left'
 
-protected theorem mul_right' (hc : 0 ≤ c) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] := by
-  rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left' hc
+protected theorem mul_right' (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] := by
+  rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left'
 #align int.modeq.mul_right' Int.ModEq.mul_right'
 
 protected theorem add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] :=
@@ -179,16 +194,11 @@ protected theorem sub_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a - c ≡ b - c [
 #align int.modeq.sub_right Int.ModEq.sub_right
 
 protected theorem mul_left (c : ℤ) (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD n] :=
-  match (le_total 0 c) with
-  | .inl hc => (h.mul_left' hc).of_dvd (dvd_mul_left _ _)
-  | .inr hc => by
-    rw [← neg_neg c, neg_mul, neg_mul _ b]
-    exact ((h.mul_left' <| neg_nonneg.2 hc).of_dvd (dvd_mul_left _ _)).neg
+  h.mul_left'.of_dvd <| dvd_mul_left _ _
 #align int.modeq.mul_left Int.ModEq.mul_left
 
-protected theorem mul_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n] := by
-  rw [mul_comm a, mul_comm b]
-  exact h.mul_left c
+protected theorem mul_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n] :=
+  h.mul_right'.of_dvd <| dvd_mul_right _ _
 #align int.modeq.mul_right Int.ModEq.mul_right
 
 protected theorem mul (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] :=
@@ -209,6 +219,29 @@ lemma of_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
   mul_comm m n ▸ of_mul_left _
 #align int.modeq.of_mul_right Int.ModEq.of_mul_right
 
+/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
+theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
+  by
+  letI d := gcd m c
+  have hmd := gcd_dvd_left m c
+  have hcd := gcd_dvd_right m c
+  rw [modEq_iff_dvd] at h ⊢
+  -- porting note: removed `show` due to leanprover-community/mathlib4#3305
+  refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
+  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
+    exact Int.ediv_dvd_ediv hmd h
+  · rw [gcd_div hmd hcd, natAbs_ofNat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
+#align int.modeq.cancel_right_div_gcd Int.ModEq.cancel_right_div_gcd
+
+/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
+theorem cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
+  cancel_right_div_gcd hm <| by simpa [mul_comm] using h
+#align int.modeq.cancel_left_div_gcd Int.ModEq.cancel_left_div_gcd
+
+theorem of_div (h : a / c ≡ b / c [ZMOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
+    a ≡ b [ZMOD m] := by convert h.mul_left' <;> rwa [Int.mul_ediv_cancel']
+#align int.modeq.of_div Int.ModEq.of_div
+
 end ModEq
 
 theorem modEq_one : a ≡ b [ZMOD 1] :=
@@ -219,6 +252,18 @@ theorem modEq_sub (a b : ℤ) : a ≡ b [ZMOD a - b] :=
   (modEq_of_dvd dvd_rfl).symm
 #align int.modeq_sub Int.modEq_sub
 
+@[simp]
+theorem modEq_zero_iff : a ≡ b [ZMOD 0] ↔ a = b := by rw [ModEq, emod_zero, emod_zero]
+#align int.modeq_zero_iff Int.modEq_zero_iff
+
+@[simp]
+theorem add_modEq_left : n + a ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp
+#align int.add_modeq_left Int.add_modEq_left
+
+@[simp]
+theorem add_modEq_right : a + n ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp
+#align int.add_modeq_right Int.add_modEq_right
+
 theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℤ} (hmn : m.natAbs.coprime n.natAbs) :
     a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n] :=
   ⟨fun h => by
diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean
index cc0241059a764..694c76a385dad 100644
--- a/Mathlib/Data/Nat/ModEq.lean
+++ b/Mathlib/Data/Nat/ModEq.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.modeq
-! leanprover-community/mathlib commit 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -212,6 +212,10 @@ For cancelling right multiplication on both sides of the `≡`, see `nat.modeq.m
 lemma of_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] := mul_comm m n ▸ of_mul_left _
 #align nat.modeq.of_mul_right Nat.ModEq.of_mul_right
 
+theorem of_div (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
+    a ≡ b [MOD m] := by convert h.mul_left' c <;> rwa [Nat.mul_div_cancel']
+#align nat.modeq.of_div Nat.ModEq.of_div
+
 end ModEq
 
 lemma modEq_sub (h : b ≤ a) : a ≡ b [MOD a - b] := (modEq_of_dvd $ by rw [Int.ofNat_sub h]).symm
diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
index 55a6960f61192..e12e1f9dec26e 100644
--- a/Mathlib/Data/Nat/Order/Lemmas.lean
+++ b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.order.lemmas
-! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,7 +25,7 @@ please feel free to reorganize these two files.
 
 universe u v
 
-variable {m n k : ℕ}
+variable {a b m n k : ℕ}
 
 namespace Nat
 
@@ -205,6 +205,13 @@ theorem eq_zero_of_dvd_of_lt {a b : ℕ} (w : a ∣ b) (h : b < a) : b = 0 :=
     ((Nat.div_eq_zero_iff (lt_of_le_of_lt (zero_le b) h)).mpr h)
 #align nat.eq_zero_of_dvd_of_lt Nat.eq_zero_of_dvd_of_lt
 
+theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b := by
+  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
+  -- porting note: Needed to give an explicit argument to `mul_add_one`
+  rw [← mul_add_one n] at h
+  exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
+#align nat.le_of_lt_add_of_dvd Nat.le_of_lt_add_of_dvd
+
 @[simp]
 theorem mod_div_self (m n : ℕ) : m % n / n = 0 := by
   cases n
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index dc93273aa5bdf..b4c037068d845 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module data.zmod.basic
-! leanprover-community/mathlib commit 297619ec79dedf23525458b6bf5bf35c736fd2b8
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -34,6 +34,7 @@ This is a ring hom if the ring has characteristic dividing `n`
 
 -/
 
+open Function
 
 namespace ZMod
 
@@ -455,7 +456,7 @@ end CharEq
 end UniversalProperty
 
 theorem int_cast_eq_int_cast_iff (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [ZMOD c] :=
-  CharP.int_cast_eq_int_cast_iff (ZMod c) c a b
+  CharP.intCast_eq_intCast (ZMod c) c
 #align zmod.int_coe_eq_int_coe_iff ZMod.int_cast_eq_int_cast_iff
 
 theorem int_cast_eq_int_cast_iff' (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c :=
@@ -1051,6 +1052,8 @@ theorem prime_ne_zero (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq :
     hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]
 #align zmod.prime_ne_zero ZMod.prime_ne_zero
 
+variable {n a : ℕ}
+
 theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
     a.valMinAbs.natAbs = min a.val (n - a.val) := by
   rw [valMinAbs_def_pos]
@@ -1070,6 +1073,28 @@ theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
     apply Nat.lt_succ_self
 #align zmod.val_min_abs_nat_abs_eq_min ZMod.valMinAbs_natAbs_eq_min
 
+theorem valMinAbs_natCast_of_le_half (ha : a ≤ n / 2) : (a : ZMod n).valMinAbs = a := by
+  cases n
+  · simp
+  · simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
+      ha]
+#align zmod.val_min_abs_nat_cast_of_le_half ZMod.valMinAbs_natCast_of_le_half
+
+theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
+    (a : ZMod n).valMinAbs = a - n := by
+  cases n
+  · cases not_lt_bot ha'
+  · simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt ha', ha.not_le]
+#align zmod.val_min_abs_nat_cast_of_half_lt ZMod.valMinAbs_natCast_of_half_lt
+
+-- porting note: There was an extraneous `nat_` in the mathlib3 name
+@[simp]
+theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 := by
+  refine' ⟨fun ha => _, valMinAbs_natCast_of_le_half⟩
+  rw [← Int.natAbs_ofNat a, ← ha]
+  exact natAbs_valMinAbs_le a
+#align zmod.val_min_nat_abs_nat_cast_eq_self ZMod.valMinAbs_natCast_eq_self
+
 theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) :
     x.natAbs ≤ y.natAbs := by
   rw [int_cast_eq_int_cast_iff_dvd_sub] at he