Type coercion from nat to rat

Question

I'm stuck with this very simple lemma, and wonder what is the best way to proceed.

From mathcomp Require Import ssrint rat ssralg ssrnum.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Open Scope ring_scope.

Lemma X (n m : nat) : (n <= m)%N -> n%:Q <= m%:Q.
Proof.
rewrite -lez_nat.

Answer 1

So, _%:Q is a notation for _%:R as documented in rat.v Then doing Search _ Num.le _%:R or Search _ (_%:R <= _%:R) leads to ler_nat which is the right lemma to apply, as in:

Lemma X (n m : nat) : (n <= m)%N -> n%:Q <= m%:Q.
Proof. by move=> le_nm; rewrite ler_nat. Qed.

Answer 2

Lemma X (n m : nat) : (n <= m)%N -> n%:Q <= m%:Q.
Proof.
by rewrite -lez_nat -(ler_int rat_numDomainType).
Qed.