減少性が示せない?

一日ごろごろしてました。
ほとんど成果ないですが、引っかかっているポイントが浮かび上がってきたので、メモしておきます。

Haskell
前回の畳み込みを使った表現がまだ解決していない

Coq
4で割ると3余るならば真を返す関数が定義できない

Fixpoint is_4n_3 (n:N) : bool :=
match n with
| N0 => false
| Npos xH => false
| Npos (xO xH) => false
| Npos (xI xH) => true
| Npos n => is_4n_3 (n-3)
end.

この関数を定義しようとすると、
Recursive call to is_4n_3 has principal argument equal to "n - 3"
というエラーメッセージが。
調べたところ、Coqさんが引数の減少性をわかってくれてくれていないとのこと。

なんで n > n-3 って当たり前のことをわかってくれないのかと思ったら、
N_scopeでの引き算では 0 - 3 = 0 になるからか。
パターンマッチの文脈的に、n>3の場合を考えているんだけど、その意を汲み取ってもらえなかった
いったいどうすれば。

まあ、今やりたいことをするだけだったらmodを使えばいいのですが。

知ったことメモ
Haskell divと(/)は型が違う
糖衣構文だと思ってました汗