int.to_nat lemmas

Stream: general

[Scott Morrison]

I'm feeling sad about the lemmas about int.to_nat. Can someone suggest how to prove things like:

example (i : ℤ) : i.to_nat - 1 = (i + -1).to_nat :=
sorry

[Johan Commelin]

I try to avoid to_nat whenever I can. int.nat_abs seems to have a better API

[Johan Commelin]

But I don't know if it makes sense to use that in your application

[Yevhenii Diomidov]

example (i : ℤ) : i.to_nat - 1 = (i + -1).to_nat :=
by rcases i with (_ | _) | _; finish