feat(data/nat/basic,algebra/ring): adding two lemmas about division (#…

…385)

algebra/ring.lean

@@ -141,6 +141,13 @@ section comm_ring
 
   @[simp] lemma neg_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) :=
   ⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩
+
+  theorem dvd_add_left {a b c : α} (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
+  (dvd_add_iff_left h).symm
+
+  theorem dvd_add_right {a b c : α} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c :=
+  (dvd_add_iff_right h).symm
+
 end comm_ring
 
 class is_ring_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α → β) : Prop :=

data/nat/basic.lean

@@ -313,6 +313,12 @@ by rw [mul_comm c, mod_mul_right_div_self]
 @[simp] protected theorem dvd_one {n : ℕ} : n ∣ 1 ↔ n = 1 :=
 ⟨eq_one_of_dvd_one, λ e, e.symm ▸ dvd_refl _⟩
 
+protected theorem dvd_add_left {k m n : ℕ} (h : k ∣ n) : k ∣ m + n ↔ k ∣ m :=
+(nat.dvd_add_iff_left h).symm
+
+protected theorem dvd_add_right {k m n : ℕ} (h : k ∣ m) : k ∣ m + n ↔ k ∣ n := 
+(nat.dvd_add_iff_right h).symm
+
 protected theorem mul_dvd_mul_iff_left {a b c : ℕ} (ha : a > 0) : a * b ∣ a * c ↔ b ∣ c :=
 exists_congr $ λ d, by rw [mul_assoc, nat.mul_left_inj ha]