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.