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: Jan 29 2023 at 18:03 UTC