diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 83d3cdca5a..c3bdfebc54 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -3000,4 +3000,10 @@ protected theorem dvd_eq_false_of_mod_ne_zero {a b : Int} (h : b % a != 0) : (a
   simp [eq_of_beq] at h
   simp [Int.dvd_iff_emod_eq_zero, h]
 
+theorem ext_ediv_emod {n a b : Int} (h0 : a / n = b / n) (h1 : a % n = b % n) : a = b :=
+  (mul_ediv_add_emod a n).symm.trans (h0 ▸ h1 ▸ mul_ediv_add_emod b n)
+
+theorem ext_ediv_emod_iff (n a b : Int) : a = b ↔ a / n = b / n ∧ a % n = b % n :=
+  ⟨fun h => ⟨h ▸ rfl, h ▸ rfl⟩, fun ⟨h0, h1⟩ => ext_ediv_emod h0 h1⟩
+
 end Int
diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean
index 1f9473d8cd..95b7553b9d 100644
--- a/src/Init/Data/Nat/Div/Lemmas.lean
+++ b/src/Init/Data/Nat/Div/Lemmas.lean
@@ -241,4 +241,10 @@ theorem mod_eq_mod_iff {x y z : Nat} :
     replace h := congrArg (· % z) h
     simpa using h
 
+theorem ext_div_mod {n a b : Nat} (h0 : a / n = b / n) (h1 : a % n = b % n) : a = b :=
+  (div_add_mod a n).symm.trans (h0 ▸ h1 ▸ div_add_mod b n)
+
+theorem ext_div_mod_iff (n a b : Nat) : a = b ↔ a / n = b / n ∧ a % n = b % n :=
+  ⟨fun h => ⟨h ▸ rfl, h ▸ rfl⟩, fun ⟨h0, h1⟩ => ext_div_mod h0 h1⟩
+
 end Nat