Equal implies Less-Than-Or-Equal in Coq

Question

I'm trying to prove the simplest thing ever in Coq:

Require Import Coq.Structures.OrdersFacts.
Require Import Coq.Structures.Orders.
Lemma easy: forall a b : nat, (a = b) -> (a <= b).
Proof.
  intros.
  apply le_lteq.          (* doesn't work *)
  apply LeIsLtEq.le_lteq. (* doesn't work *)

But I get the following error:

The reference le_lteq
was not found in the current
environment.

This is a bit strange because I do see it in Coq.Structures.Orders

Answer 1

As you can see in the link you provided, the definition of le_lteq is not at top-level, but hidden behind other modules. The general solution when faced with this problem is to use Locate.

Locate le_lteq.

will tell you which definitions (in scope, that is available after Require) have that name and how to call them.

Note that it also works with notations.

Locate "=".

---

In this particular case, it will not work indeed because le_lteq is not only hidden behind modules, but behind functors. For instance it appears in

Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
 Include O.
 Definition le x y := x<y \/ x==y.
 Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y.
End OT_to_Full.

Meaning you would have to instantiate OT_to_Full with a module of type OrderedType'.

If there is no particular reason to use Coq.Structures.Orders then I would rather look for a lemma on natural numbers directly.

Search "=" "<=".

does not yield what you want. Instead we will use subst b to replace b with a in the goal. And this is fine because we have a proof of a <= a which we find using

Search (?x <= ?x).

which prints

le_n: forall n : nat, n <= n

The proof is then:

Lemma easy :
  forall (a b : nat),
    a = b ->
    a <= b.
Proof.
  intros a b e.
  subst b.
  apply le_n.
Qed.