COQ: How to use "<=" for Z and R in the same lemma?

user_13548228 0
Viewed 45

Suppose I already defined floor (from R to Z). Now I want to prove that n <= x implies n <= floor(x), where n : Z, x : R.

I tried:

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

but I'm getting the error The term n has type Z while it is expected to have type R.

How should I write this? Is there a way that I can use <= for Z and R simultaneously?

coq
1 Answers

In order to override the default interpretation of a notation, you can open a notation scope locally using %key:

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