The Coq mailing list

[Yves Bertot <Yves.Bertot AT inria.fr>]

On 10/24/2016 01:10 PM, Klaus Ostermann wrote:
> I feel a bit stupid to ask this, but how does one use all the nice Lemmas
> (like, say, max_id : max m m = m) in GenericMinMax specialized to the
> type "nat"?
>
> Presumably I have to do some kind of functor/module composition, but I
> don't
> know how and I also can't find any preexisting examples. Or
> do they exist in some pre-configured form in the standard library?
>
> Klaus
They exist in some pre-configured form in the library Arith, for 
instance.  Try the following commands:

Require Import Arith.
Locate max_id.

Yves