feat: characterize when T-division equals zero

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -1340,6 +1340,42 @@ theorem sign_tdiv (a b : Int) : sign (a.tdiv b) = if natAbs a < natAbs b then 0
   | _, _, ⟨_, .inr rfl⟩, ⟨_, .inl rfl⟩ => by rw [Int.neg_tdiv, natAbs_neg, natAbs_neg]; rfl
   | _, _, ⟨_, .inr rfl⟩, ⟨_, .inr rfl⟩ => by rw [Int.neg_tdiv_neg, natAbs_neg, natAbs_neg]; rfl
 
+/-- T-division of an integer by a natural number equals zero iff
+the absolute value of the numerator is less than the denominator.
+-/
+theorem tdiv_ofNat_eq_zero_iff_natAbs_lt_or_eq_zero {a : Int} {b : Nat} :
+    a.tdiv b = 0 ↔ (a.natAbs < b ∨ b = 0) := by
+  rcases b with _|b
+  · simp
+  · simp only [natCast_add, cast_ofNat_Int, Nat.add_eq_zero, Nat.succ_ne_self, and_false, or_false]
+    suffices ∀ (a : Nat), (a : Int).tdiv (↑b + 1) = 0 ↔ a < b + 1 by
+      rcases a with _|a
+      · simpa using this _
+      · obtain ⟨n, hn⟩ := exists_eq_neg_ofNat (show -[a+1] ≤ 0 by omega)
+        simp [hn, this]
+        apply this
+    intro a
+    rw [Int.tdiv_eq_ediv_of_nonneg (by omega)]
+    norm_cast
+    apply Nat.div_eq_zero_iff_lt (by omega)
+
+/-- T-divison equals zero iff the absolute value of the numerator is less
+than the absolute value of the denominator, or the denominator is zero.
+-/
+@[simp] theorem tdiv_eq_zero_iff_natAbs_lt_or_eq_zero {a : Int} {b : Int} :
+    a.tdiv b = 0 ↔ (a.natAbs < b.natAbs ∨ b = 0):= by
+  have hb := Int.lt_trichotomy b 0
+  rcases hb with hb | rfl | hb
+  · obtain ⟨b, rfl⟩ := exists_eq_neg_ofNat (show b ≤ 0 by omega)
+    rw [Int.tdiv_neg]
+    simp only [Int.neg_eq_zero, natAbs_neg, natAbs_natCast]
+    norm_cast
+    apply Int.tdiv_ofNat_eq_zero_iff_natAbs_lt_or_eq_zero
+  · simp
+  · obtain ⟨b, rfl⟩ := eq_ofNat_of_zero_le (show 0 ≤ b by omega)
+    norm_cast
+    apply Int.tdiv_ofNat_eq_zero_iff_natAbs_lt_or_eq_zero
+
 /-! ### tmod -/
 
 -- `tmod` analogues of `emod` lemmas from `Bootstrap.lean`