How do I use results proven in a given library? For example, I want to use Lemma peano_ind from the library BinInt. I write this in CoqIDE:
Require Import BinInt.
Check peano_ind.
and get a "The reference peano_ind was not found in the current
environment." error. I am also not able to use it with apply during a proof.
However, it should be there, because with a Locate Library BinInt. I see that Coq can find the file BinInt.vo, and when I open the file BinInt.v I can see Lemma peano_ind.
I have this exact problem both on a Debian 9.0 + CoqIDE 8.5pl2 and on a Windows 10 + CoqIDE 8.6.
All of this because I wanted to do induction over the integers. A different solution for that would also be nice, but I'm still frustrated by my lack of ability to use some previously proven results.