Ошибка в определении Аккермана в Coq

Я пытаюсь определить функцию Аккермана -Петерса в Coq и получаю сообщение об ошибке, которого не понимаю. Как видите, я упаковываю аргументы a, bАккермана в пару ab; Я предоставляю упорядочивание, определяющее функцию упорядочивания аргументов. Затем я использую форму Functionдля определения самого Аккермана, предоставляя ему функцию упорядочения для аргумента ab.

Require Import Recdef.    
Definition ack_ordering (ab1 ab2 : nat * nat) :=
    match (ab1, ab2) with
    |((a1, b1), (a2, b2)) => 
       (a1 > a2) \/ ((a1 = a2) /\ (b1 > b2))   
    end.
Function ack (ab : nat * nat) {wf ack_ordering} : nat :=
match ab with
| (0, b) => b + 1
| (a, 0) => ack (a-1, 1)
| (a, b) => ack (a-1, ack (a, b-1))
end.

Я получаю следующее сообщение об ошибке:

Ошибка :Нет такой переменной раздела или предположения:ack.

Не знаю, что беспокоит Coq, но поискав в Интернете, я нашел предположение, что может возникнуть проблема с использованием рекурсивной функции, определенной с помощью упорядочения или меры, когда рекурсивный вызов происходит внутри совпадения. Однако использование проекций fstи sndи if-then-elseпривело к другому сообщению об ошибке. Может кто-нибудь предложить, как определить Аккермана в Coq?