COQ：如何在同一引理中对 Z 和 R 使用“<=”？

Question

假设我已经定义了floor(fromR到Z)。现在我想证明这n <= x意味着n <= floor(x)，哪里n : Z，x : R。

我试过：

Lemma l: forall (n:Z) (x:R), (IZR n) <= x -> n <= (floor x).

但我收到错误The term n has type Z while it is expected to have type R.

我该怎么写这个？有没有一种方法可以同时<=使用？ZR

Answer 1

为了覆盖符号的默认解释，您可以使用以下命令在本地打开符号范围%key：

Lemma l : forall n x, (IZR n <= x)%R -> (n <= floor x)%Z.