Is there a way to automatically prove simple inequalities like 1/2 >= 0?, i.e.
Require Export Coq.Reals.RIneq.
Local Open Scope Z_scope.
Local Open Scope R_scope.
Example test: /2 >= 0.
I haven't much experience with ring or field, and I am having trouble with even proving simple equalities such as 1/2 = 2/4.
What I am looking for is something like omega but works for real numbers and inequalities.
The tools you are looking for are described in the chapter on Omega of the reference manual and deal with various arithmetic goals over ordered rings: (non)-linear integer arithmetic, and linear rational / real arithmetic.
They are defined in the Psatz module and may require you to install some external solvers. In this case, lra does not (AFAICT) have external dependencies and discharges the test goal.