I'm trying to prove
Theorem T20d :forall (x y:R), (0<x /\ 0<y) -> 0 < Rmin x y.
with
Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m.
which is in Coq.Structures.GenericMinMax
which I imported with Require Import Coq.Structures.GenericMinMax
however, I still get "reference min_glb_lt" not found when I try to use it? I suspect I need to open a scope, but I don't know which scope.
First of all, the
GenericMinMax
library defines generic structures, so you can't use them directly to solve a concrete problem. That library mostly contains functors. In other words, it provides interfaces which you need to implement to be able to use them.In our case, we need to implement the
MinMaxLogicalProperties
functor (or some other functor that includes this one), because it includes the required lemma.Several Coq standard libraries provide such implementations. Luckily for us, it has already been done for the reals in the file
Rminmax.v
, inside the moduleR
, this line specifically:So, we can use it like so:
Alternatively, we could've referred to the lemma by its qualified name
R.min_glb_lt
-- that would've let us get rid ofImport R
.