From dbaf8f03adb463f7902867581154ef3561ff3fd3 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 14 Dec 2023 13:50:35 +1100
Subject: [PATCH] feat: emod_pos_of_not_dvd for Nat and Int (#436)

---
 Std/Data/Int/DivMod.lean | 5 +++++
 Std/Data/Nat/Lemmas.lean | 4 ++++
 2 files changed, 9 insertions(+)

diff --git a/Std/Data/Int/DivMod.lean b/Std/Data/Int/DivMod.lean
index 61cf32b22c..3d0a11d8b5 100644
--- a/Std/Data/Int/DivMod.lean
+++ b/Std/Data/Int/DivMod.lean
@@ -719,6 +719,11 @@ theorem dvd_iff_mod_eq_zero (a b : Int) : a ∣ b ↔ mod b a = 0 :=
 theorem dvd_iff_emod_eq_zero (a b : Int) : a ∣ b ↔ b % a = 0 :=
   ⟨emod_eq_zero_of_dvd, dvd_of_emod_eq_zero⟩
 
+theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a := by
+  rw [dvd_iff_emod_eq_zero] at h
+  if w : a = 0 then simp_all
+  else exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)
+
 instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
   decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero ..).symm
 
diff --git a/Std/Data/Nat/Lemmas.lean b/Std/Data/Nat/Lemmas.lean
index acd0bcfae6..f6cec33a7e 100644
--- a/Std/Data/Nat/Lemmas.lean
+++ b/Std/Data/Nat/Lemmas.lean
@@ -1204,6 +1204,10 @@ theorem mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) : n % m = 0 := by
 theorem dvd_iff_mod_eq_zero (m n : Nat) : m ∣ n ↔ n % m = 0 :=
   ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
 
+theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by
+  rw [dvd_iff_mod_eq_zero] at h
+  exact Nat.pos_of_ne_zero h
+
 instance decidable_dvd : @DecidableRel Nat (·∣·) :=
   fun _ _ => decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero _ _).symm