int.coe_to_nat_eq

Stream: Is there code for X?

[Eloi]

I didn't find this in the library... Is there some similar lemma?

example (n:ℤ): 0 ≤ n → ↑(n.to_nat) = n :=
  begin
    sorry,
  end

[Rob Lewis]

docs#int.to_nat_of_nonneg

[Rob Lewis]

library_search finds this (if you have data.int.basic imported)

[Eloi]

Thaks, I was searching manually in lib/lean/library/init/data.int.basic and I thought it was mathlib.