Int.natAbs of nonzero is nonzero?

Stream: lean4

[Omnikar]

Hi. Is there a built-in theorem I can use for showing that Int.natAbs of a nonzero integer gives a nonzero natural? If not, how can I write one myself?

[Ruben Van de Velde]

Certainly in mathlib, likely in std4. exact? or apply? likely finds it

[Riccardo Brasca]

docs#Int.natAbs_ne_zero says exactly that

[Omnikar]

Thanks.