Commit 2021-02-17 11:38 b190131f

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.