feat(lint): improved ge_or_gt linter (#3810)
The linter will now correctly accepts occurrences of `f (≥)` and `∃ x ≥ t, b`
The linter will still raise a false positive on `∃ x y ≥ t, b` (with 2+ bound variables in a single binder that involves `>/≥`)
In contrast to the previous version of the linter, this one *does* check hypotheses.
This should reduce the `@[nolint ge_or_gt]` attributes from ~160 to ~10.
