Agda的“重写”失败,出现一个提到变量“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表示:

c*d!=w型
检查类型时
(c d w:)
w d*c
(a:)(x:c>0)(y:d>0)
a÷wŸ¨x*>0 y–aÃd*c–y*>0 x–Ÿ)
函数的生成形式良好