diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3611e9e06f..66f54d9240 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -375,6 +375,7 @@ Additions to existing modules
 
 * In `Data.Nat.Divisibility`:
   ```agda
+  ∣m+n∣n⇒∣m : d ∣ m + n → d ∣ n → d ∣ m
   m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o
   n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o
   ```
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index cba883efab..1115f339db 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -190,13 +190,21 @@ n∣n = ∣-refl
 ∣m+n∣m⇒∣n : d ∣ m + n → d ∣ m → d ∣ n
 ∣m+n∣m⇒∣n {d} {m} {n} (divides p m+n≡p*d) (divides-refl q) =
   divides (p ∸ q) $ begin-equality
-    n             ≡⟨ m+n∸n≡m n m ⟨
-    n + m ∸ m     ≡⟨ cong (_∸ m) (+-comm n m) ⟩
+    n             ≡⟨ m+n∸m≡n m n ⟨
     m + n ∸ m     ≡⟨ cong (_∸ m) m+n≡p*d ⟩
     p * d ∸ q * d ≡⟨ *-distribʳ-∸ d p q ⟨
     (p ∸ q) * d   ∎
     where open ∣-Reasoning
 
+∣m+n∣n⇒∣m : d ∣ m + n → d ∣ n → d ∣ m
+∣m+n∣n⇒∣m {d} {m} {n} (divides p m+n≡p*d) (divides-refl q) =
+  divides (p ∸ q) $ begin-equality
+    m             ≡⟨ m+n∸n≡m m n ⟨
+    m + n ∸ n     ≡⟨ cong (_∸ q * d) m+n≡p*d ⟩
+    p * d ∸ q * d ≡⟨ *-distribʳ-∸ d p q ⟨
+    (p ∸ q) * d   ∎
+  where open ∣-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _∣_ and _*_