feat(data/int/cast/lemmas): a.nat_mod b < b (#17896)

YaelDillies · eric-wieser · YaelDillies · commit 7a89b1aed52b · 2023-01-06T07:59:14.000Z
The modulus of an integer by a natural is strictly less than the natural.



Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
diff --git a/src/data/int/cast/lemmas.lean b/src/data/int/cast/lemmas.lean
@@ -36,6 +36,12 @@ def of_nat_hom : ℕ →+* ℤ := ⟨coe, rfl, int.of_nat_mul, rfl, int.of_nat_a
 
 lemma coe_nat_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) := int.coe_nat_pos.2 (succ_pos n)
 
+lemma to_nat_lt {a : ℤ} {b : ℕ} (hb : b ≠ 0) : a.to_nat < b ↔ a < b :=
+by { rw [←to_nat_lt_to_nat, to_nat_coe_nat], exact coe_nat_pos.2 hb.bot_lt }
+
+lemma nat_mod_lt {a : ℤ} {b : ℕ} (hb : b ≠ 0) : a.nat_mod b < b :=
+(to_nat_lt hb).2 $ mod_lt_of_pos _ $ coe_nat_pos.2 hb.bot_lt
+
 section cast
 
 @[simp, norm_cast] theorem cast_mul [non_assoc_ring α] : ∀ m n, ((m * n : ℤ) : α) = m * n :=
