从 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

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

Answer 2

因此，_%:Q 是 _%:R 的一种表示法，如记录 in rat.v 然后做 Search _ Num.le _%:R 或 Search _ (_%: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.

从 nat 到 rat 的强制类型

Type coercion from nat to rat

coq

ssreflect