Add greater or equal symbol for numbers

I feel it is sometime clearer to write x ≥ y than y ≤ x in certain specific cases such as

match order with
 | Lt => x < y
 | Le => x ≤ y
 | Gt => x > y
 | Ge => x ≥ y
end

So I added ≥ as an infix for the numbers, as well as (>) and (≥)

If that feeling is not shared, I'm happy to keep those for my own developments.

Not ever using > or ≥ is a deliberate choice that we should document better. The problem is that if you have x < y in the context and need y > x for some lemma, assumption won't work, and it's just generally very frustrating to deal with this mismatch. It is preferable to state logically equivalent things in syntactically equal ways.

I think your development will also benefit from that choice.

What Ralf said.

I think it's a bad choice in the Coq stdlib that x > y is not just syntactic sugar for y < x. For most number types the two are not even definitionally equal!

If we want to have ≥ and > I would be better to have them as only parsing, which is what math-comp is doing https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v#L323 But that will overwrite notations from the stdlib, so I am not super enthusiastic about that either.

That choice makes sense, but adding a comment explaining it might be good, because when I looked at the good was "nobody needed it yet" and not "They didn't add it deliberately". I think I'll stick to this choice to from now on

closed

mentioned in merge request !500 (merged)