The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 10/21/2016 12:02 AM, Patricia Peratto wrote:
>     I want to use proofs from the Library NOrder.
>
>     I get the message:
>
>     Error: The reference le_0_r was not found
>     in the current environment.
>     The same with other proofs.
>
>     Is there other library that includes  the proofs of NOrder?
>
>     Regards
>     Patricia


Require Import PeanoNat.


Locate le_0_r.

(*
    Constant Coq.Arith.PeanoNat.Nat.le_0_r
     (shorter name to refer to it in current context is Nat.le_0_r)
*)


Check Nat.le_0_r.