There is a theory for rationals within the reals. Is there a similar theory and hints database for the integers?
@Vincent Semeria ?
Found it, but the rewrite database seems to be absent:
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