feat(data/nat/(basic, modeq)): simple lemmas (#8647)

src/data/nat/basic.lean

@@ -644,6 +644,9 @@ begin
     exact nat.le_of_pred_lt h', },
 end
 
+@[simp] lemma add_sub_sub_cancel {a c : ℕ} (h : c ≤ a) (b : ℕ) : a + b - (a - c) = b + c :=
+by rw [add_comm, nat.add_sub_assoc (nat.sub_le_self _ _), nat.sub_sub_self h]
+
 /-! ### `mul` -/
 
 lemma succ_mul_pos (m : ℕ) (hn : 0 < n) : 0 < (succ m) * n :=
@@ -943,6 +946,12 @@ by rw [mul_comm, nat.eq_mul_of_div_eq_right H1 H2]
 protected theorem mul_div_cancel_left' {a b : ℕ} (Hd :  a ∣ b) : a * (b / a) = b :=
 by rw [mul_comm,nat.div_mul_cancel Hd]
 
+/-- Alias of `nat.mul_div_mul` -/ --TODO: Update `nat.mul_div_mul` in the core?
+protected lemma mul_div_mul_left (a b : ℕ) {c : ℕ} (hc : 0 < c) : c * a / (c * b) = a / b :=
+nat.mul_div_mul a b hc
+protected lemma mul_div_mul_right (a b : ℕ) {c : ℕ} (hc : 0 < c) : a * c / (b * c) = a / b :=
+by rw [mul_comm, mul_comm b, a.mul_div_mul_left b hc]
+
 /-! ### `mod`, `dvd` -/
 
 lemma div_add_mod (m k : ℕ) : k * (m / k) + m % k = m :=

src/data/nat/modeq.lean

@@ -168,6 +168,14 @@ end)
 
 end modeq
 
+@[simp] lemma modeq_zero_iff {a b : ℕ} : a ≡ b [MOD 0] ↔ a = b :=
+by rw [nat.modeq, nat.mod_zero, nat.mod_zero]
+
+@[simp] lemma add_modeq_left {a n : ℕ} : n + a ≡ a [MOD n] :=
+by rw [nat.modeq, nat.add_mod_left]
+@[simp] lemma add_modeq_right {a n : ℕ} : a + n ≡ a [MOD n] :=
+by rw [nat.modeq, nat.add_mod_right]
+
 @[simp] lemma mod_mul_right_mod (a b c : ℕ) : a % (b * c) % b = a % b :=
 modeq.modeq_of_modeq_mul_right _ (modeq.mod_modeq _ _)