## Stream: math-comp users

### Topic: ssrint

#### Marie Kerjean (Feb 18 2021 at 20:45):

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.

#### Pierre-Yves Strub (Feb 18 2021 at 20:45):

What do you mean. That you want to get a `nat` from `x`?

#### Pierre-Yves Strub (Feb 18 2021 at 20:46):

In that case, `case: x le0x => // x _` will do it.

#### Marie Kerjean (Feb 18 2021 at 20:55):

Thanks ! So `Znat` is here for a whole other purpose ?

#### Pierre-Yves Strub (Feb 18 2021 at 21:12):

Well, `Znat` is transparent enough s.t. the above tactic works when `le0x : x \is a Znat`

#### Pierre-Yves Strub (Feb 18 2021 at 21:16):

And if you want to use `ZnatP`, you can do that: `case/ZnatP: le0x => [n {x}->].`

#### Cyril Cohen (Feb 18 2021 at 21:20):

And if you are not inside a proof you can use ` `|x|%N` instead

#### Marie Kerjean (Feb 18 2021 at 21:36):

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 ?

#### Cyril Cohen (Feb 18 2021 at 21:44):

Yes: ` `|x|%N`

#### Marie Kerjean (Feb 18 2021 at 22:03):

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: Jul 15 2024 at 20:02 UTC