Agda的`rewrite`失败，并出现错误，提及变量“ w”

我有这些定义（不相关的定义已删除）

open import Agda.Builtin.Nat renaming (Nat to ℕ)

infix 3 _>0
data _>0 : ℕ → Set where
  intro : ∀ n → suc n >0

infix 4 _*>0_
_*>0_ : ∀ {a b} → a >0 → b >0 → a * b >0
intro n *>0 intro m = intro (m + n * suc m)

infix 5 _÷_⟨_⟩
data ℚ : Set where
  _÷_⟨_⟩ : (a b : ℕ) → b >0 → ℚ

我想证明这是真的：

open import Agda.Builtin.Equality

div-mul-comm : ∀ a c d → (x : c >0) → (y : d >0) →
               a ÷ c * d ⟨ x *>0 y ⟩ ≡ a ÷ d * c ⟨ y *>0 x ⟩
div-mul-comm a c d x y = ?

但是无论我如何尝试，都无法证明这一点，错误消息也很奇怪。
这是我尝试过的：

postulate nat-multiply-comm : ∀ a b → a * b ≡ b * a

div-mul-comm a c d x y
  rewrite nat-multiply-comm c d = {!!}

阿格达（Agda）说：

当检查类型
（cdw：ℕ）→
w d * c→
（a：ℕ）（x：c> 0）（y：d> 0）→
a÷wℕ时，c * d！= of的w x *> 0 y≡a÷d * c y *> 0 x
生成的with函数格式正确