Hello!

In mathcomp book we have such a definition

```
Definition edivn_rec d :=
fix loop m q := if m - d is m'.+1 then loop m' q.+1 else (q, m).
```

It looks to me like `m'`

is not a direct subterm of `m`

(at least it is not obvious (isn't it??)).

Why then the guard does not complain here?

I was able to find this one https://proofassistants.stackexchange.com/questions/1428/formal-description-of-coq-s-termination-checker

if somebody can give a link to simpler description, would be great still.

The positivity checker is able to find that `Nat.sub m d`

is a subterm of `m`

thanks to the way `Nat.sub`

is written.

Last updated: Jul 15 2024 at 19:01 UTC