Division and comparison in SMT and Alt-ergo
It seems that we have no lemmas that relate real division and comparison. It is the case for provers that doesn't have built-in these symbol because /.
is defined with inv
and *.
, and because *.
is said monotone.