coq - 类型强制从 nat 到 rat

Question

我被这个非常简单的引理所困扰，想知道最好的方法是什么。

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

因此，_%:Q是一个记号，_%:R如 Then doing or中所记录的那样rat.v，哪个是适用的正确引理，如：Search _ Num.le _%:RSearch _ (_%:R <= _%:R)ler_nat

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.