There is a theory for rationals within the reals. Is there a similar theory and hints database for the integers?

https://coq.inria.fr/library/Coq.QArith.Qreals.html

@Vincent Semeria ?

Found it, but the rewrite database seems to be absent:

https://github.com/coq/coq/blob/master/theories/Reals/RIneq.v

I have never used hints or proof automation. What do you want to do with those theorems in RIneq ?

In general, to write proofs in Coq with the convenient of proving theorems on paper.

Last updated: Feb 06 2023 at 07:03 UTC