feat(data/nat/basic): add a few lemmas (#14718)

Add a few lemmas about sub and mod.

Author: user7230724

src/algebra/order/sub.lean

@@ -439,6 +439,9 @@ end
 lemma tsub_tsub_tsub_cancel_right (h : c ≤ b) : (a - c) - (b - c) = a - b :=
 by rw [tsub_tsub, add_tsub_cancel_of_le h]
 
+lemma tsub_lt_of_lt (h : a < b) : a - c < b :=
+lt_of_le_of_lt tsub_le_self h
+
 /-! ### Lemmas that assume that an element is `add_le_cancellable`. -/
 
 namespace add_le_cancellable

src/data/nat/basic.lean

@@ -1289,6 +1289,15 @@ lemma dvd_left_injective : function.injective ((∣) : ℕ → ℕ → Prop) :=
 lemma div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / d < b / d :=
 by { rw nat.lt_div_iff_mul_lt hdb, exact lt_of_le_of_lt (mul_div_le a d) h }
 
+lemma mul_add_mod (a b c : ℕ) : (a * b + c) % b = c % b :=
+by simp [nat.add_mod]
+
+lemma mul_add_mod_of_lt {a b c : ℕ} (h : c < b) : (a * b + c) % b = c :=
+by rw [nat.mul_add_mod, nat.mod_eq_of_lt h]
+
+lemma pred_eq_self_iff {n : ℕ} : n.pred = n ↔ n = 0 :=
+by { cases n; simp [(nat.succ_ne_self _).symm] }
+
 /-! ### `find` -/
 section find