## Stream: general

### Topic: int.to_nat lemmas

#### Scott Morrison (Feb 13 2021 at 08:39):

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 (Feb 13 2021 at 08:57):

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

#### Johan Commelin (Feb 13 2021 at 08:57):

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

#### Yevhenii Diomidov (Feb 13 2021 at 19:55):

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


Last updated: May 09 2021 at 19:11 UTC