Mastodawn

when negating an inequality, you flip the strictness:
!(x >= y) <=> x < y
!(x > y) <=> x <= y

but when simply flipping around an inequality, you don't:
x > y <=> y < x
x >= y <=> y <= x

why do I have to think about these every time, or else I mix them up???

btw playing with stuff like this in Lean is a joy

import Mathlib

example (x y : Real) : ¬ x >= y ↔ x < y := by
exact not_le

example (x y : Real) : ¬ x > y ↔ x <= y := by
exact not_lt

example (x y : Real) : x > y ↔ y < x := by
rfl

example (x y : Real) : x >= y ↔ y <= x := by
rfl

@regehr have you discovered grind yet?

@bhargavkk yes! but at my stage I don't think it's a good idea to use it too much since then I can't learn anything

@regehr for real numbers ok, but not for float or double including NANs!