Agda: Failed to solve the following constraints when solve divison property

I have code below:

module div where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-assoc)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; sym; trans)

data _∣_ : ℕ → ℕ → Set where
    0∣0 : zero ∣ zero
    m∣0 : ∀ {d} → suc d ∣ zero
    m∣n : ∀ {d m} → suc d ∣ m → suc d ∣ suc (m + d)

infix 4 _∣_

∣-refl : ∀ a → a ∣ a
∣-refl zero = 0∣0
∣-refl (suc a) = m∣n m∣0

+zero : ∀ m → m + zero ≡ m
+zero zero = refl
+zero (suc m) rewrite +zero m = refl

+n : ∀ {m n : ℕ} → m + suc n ≡ suc (m + n)
+n {zero} {n} = refl
+n {suc m} {n} = cong suc (+n)

d-suc : ∀ {m n : ℕ} → suc (m + suc n) ≡ suc (suc (m + n))
d-suc = cong suc (+n)


∣-plus : ∀ a b c → a ∣ b → a ∣ c → a ∣ b + c
∣-plus .zero .zero c 0∣0 r₂ = r₂
∣-plus .(suc _) .zero c m∣0 r₂ = r₂
∣-plus _ (suc w) .zero (m∣n r₁) m∣0 rewrite +zero w = m∣n r₁
∣-plus (suc d) .(suc (_ + _)) .(suc (_ + _)) (m∣n r₁) (m∣n r₂) = {!   !} 

Run agda and it shows errors for last line.

Failed to solve the following constraints:
  _63 + _64 = m + d : ℕ (blocked on _63)
  _61 + _62 = m₁ + d : ℕ (blocked on _61)

I try to make the last line look like this,

∣-plus (suc d) (suc (m₁ + d)) (suc (m₂ + d)) (m∣n r₁) (m∣n r₂) = ?

So the goal should be ?0 : suc d ∣ suc (m₁ + d + suc (m₂ + d)), then I can get new goal ?0 : suc (suc(m₁ + d + (m₂ + d))) by d-suc. Now if i can prove

suc (suc(m₁ + d + (m₂ + d))) ≡ suc (suc(m₁ + m₂ + d + d))

where right side is m∣n (m∣n (∣-plus _ _ _ r₁ r₂)), then it is finished. But I can not get the m₁ and m₂ because above errors. How to solve it ? or my proof method is wrong ?

EDIT:
The proof can be simplifed

∣-plus : ∀ a b c → a ∣ b → a ∣ c → a ∣ b + c
∣-plus .zero .zero c 0∣0 r₂ = r₂
∣-plus .(suc _) .zero c m∣0 r₂ = r₂
∣-plus .(suc _) .(suc _) c (m∣n r₁) r₂ = ?

The goal is 0? : suc d ∣ suc (m + d + c), we can get suc d ∣ suc (m + c + d) by m∣n (∣-plus _ _ _ r₁ r₂). But it still requires d and m are available to give the equality m + d + c = m + c + d.

EDIT2:

I add a new equality

open import Data.Nat.Properties using (+-assoc; +-comm; +-identityʳ)

++ex : ∀ {a b c : ℕ} → a + b + c ≡ a + c + b
++ex {zero} {b} {c} rewrite +-comm b c = refl
++ex {suc a} {b} {c} = cong suc (++ex {a} {b} {c})

∣-plus : ∀ a b c → a ∣ b → a ∣ c → a ∣ b + c
∣-plus .zero .zero c 0∣0 r₂ = r₂
∣-plus .(suc _) .zero c m∣0 r₂ = r₂
∣-plus (suc d) .(suc _) c (m∣n r₁) r₂ with m∣n (∣-plus _ _ _ r₁ r₂)
... | s rewrite ++ex {_} {c} {d} = {!  !}

But I still can not get the m to apply this equality.

Using functions in patterns is not supported from the post "could-not-parse-the-left-hand-side"

Thus I solve it by refl, it is really powerful. Here is my full code

module div where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-assoc; +-comm; +-identityʳ)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; sym; trans)

data _∣_ : ℕ → ℕ → Set where
    0∣0 : zero ∣ zero
    m∣0 : ∀ {d} → suc d ∣ zero
    m∣n : ∀ {d m} → suc d ∣ m → suc d ∣ suc (m + d)

infix 4 _∣_

++ex : ∀ {a b c : ℕ} → a + b + c ≡ a + c + b
++ex {zero} {b} {c} rewrite +-comm b c = refl
++ex {suc a} {b} {c} = cong suc (++ex {a} {b} {c})

++ex1 : ∀ {d m c w} → w ≡ m + d → w + c ≡ m + c + d
++ex1 {d} {m} {c} {.(m + d)} refl = ++ex {m} {d} {c}  

∣-plus : ∀ a b c → a ∣ b → a ∣ c → a ∣ b + c
∣-plus .zero .zero c 0∣0 r₂ = r₂
∣-plus .(suc _) .zero c m∣0 r₂ = r₂
∣-plus (suc d) (suc w) c (m∣n r₁) r₂ with m∣n (∣-plus _ _ _ r₁ r₂)
... | s rewrite ++ex1 {d} {_} {c} {w} refl = s