Hey. I just got this in some goal:
c 0.+1 (coq 8.13.0 & mathcomp 1.12.0). Seems pretty weird.
Hmmm. Got it. The
0 was from
I really dislike the notations
Order. I would strongly vote for
top or something similar. For example, I formalized the weak order on the symmetric group. The smallest element
0%O is the identity permutation
1%G. It was very confusing.
In any case, in the
0%N should be preferred over
Last updated: Feb 08 2023 at 04:04 UTC