How do I handle x : int
for which I know that 0 <= x
as an element of type nat
? I'm sure it's obvious but for a reason I can't find it in ssrint.
What do you mean. That you want to get a nat
from x
?
In that case, case: x le0x => // x _
will do it.
Thanks ! So Znat
is here for a whole other purpose ?
Well, Znat
is transparent enough s.t. the above tactic works when le0x : x \is a Znat
And if you want to use ZnatP
, you can do that: case/ZnatP: le0x => [n {x}->].
And if you are not inside a proof you can use `|x|%N
instead
Pierre-Yves Strub said:
In that case,
case: x le0x => // x _
will do it.
Is there a way to do that do that x : nat
is not opaque ?
Yes: `|x|%N
Thanks ! For the record I was trying to get out an ugly mixture between Rfloor
Rtoint
and nat
, using the floor of a positive real as a nat, but I did not manage at the end : https://github.com/math-comp/analysis/blob/8f51f8711e896f99859a9856597d1ce377ecb0bd/theories/banach_steinhaus.v#L144.
Last updated: Oct 13 2024 at 01:02 UTC