feat(data/int/basic): lemmas about int and int.to_nat (#6253)
Golfing welcome.
This adds a `@[simp]` lemma `int.add_minus_one : i + -1 = i - 1`, which I think is mostly helpful, but needs to be turned off in `data/num/lemmas.lean`, which is perhaps an argument against it.
I've also added a lemma
```
@[simp] lemma lt_self_iff_false [preorder α] (a : α) : a < a ↔ false :=
```
(not just for `int`), which I've often found useful (e.g. `simpa` works well when it can reduce a hypothesis to `false`). This lemma seems harmless, but I'm happy to hear objections if it is too general.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
