whenever I require-open `ssralg`

and `ssrnum`

and open `ring_scope`

, my usual `nat`

notations stop working. Is there a way to make them work again? For example:

```
From mathcomp.ssreflect Require Import all_ssreflect.
From mathcomp.algebra Require Import ssralg ssrnum.
Check 1%nat < 1.
Open Scope ring_scope.
Fail Check 1%nat < 1. (* The term "1" has type "nat" while it is expected to have type "Order.POrder.sort ?T". *)
Check (1 < 1)%nat. (* Works but annoying *)
```

First, we use `%N`

instead of `%nat`

.

Since mathcomp 1.11, you should always import `order`

whenever you import `ssrnum`

, otherwise you might be missing tons of important canonical structures! As soon as you do this you should be able to write `1%N < 1%N`

for example (not `1%N < 1`

, because the second `1`

would be `Ring.one`

), but I recommend you use `(1 < 1)%N`

instead in order to use `leq`

rather than `Order.lt`

to be able to rewrite with theorems from `ssrnat`

. Unfortunately, Coq notation system works top down (an argument of a notation/definition can be tagged in some scope), and not bottom up (the type / scope information of a given object cannot be used to determine the scope of a surrounding notation), and there is no way to get around this to my knowledge...

Last updated: Jul 25 2024 at 15:02 UTC