some lemmas

Stream: general

[Scott Morrison]

Any opinions on adding these?

lemma int.succ_ne_self (n : ℤ) : n + 1 ≠ n :=
λ h, one_ne_zero ((add_left_inj n).mp (by { convert h, simp }))
lemma int.pred_ne_self (n : ℤ) : n - 1 ≠ n :=
λ h, one_ne_zero (neg_inj ((add_left_inj n).mp (by { convert h, simp })))

I couldn't find them in mathlib.

[Chris Hughes]

They're true in ring with 0 \ne 1. Maybe even semiring.

[Johan Commelin]

The second doesn't make sense in a semiring... for the former you need something cancellative

[Scott Morrison]

Does int have some typeclass already that asserts 0 \ne 1?

[Scott Morrison]

example : zero_ne_one_class ℤ := infer_instance

[Johan Commelin]

There is nonzero_comm_ring. I don't think there is nonzero_ring though.

[Scott Morrison]

I'll just write the lemma with [zero_ne_one_class R] and [ring R]?

[Johan Commelin]

I think you than have two incompatible zeros?

[Johan Commelin]

And two ones...

[Scott Morrison]

... yes.

[Scott Morrison]

Okay, sorted it out. Shall I put this in a separate PR? (I'm tempted to just roll it into the PR that needs these lemmas...)

[Reid Barton]

How about

lemma int.succ_ne_self (n : ℤ) : n + 1 ≠ n :=
ne_of_gt n.lt_succ_self
lemma int.pred_ne_self (n : ℤ) : n - 1 ≠ n :=
ne_of_lt n.pred_self_lt

[Floris van Doorn]

The first one should be done for a nonzero_comm_semiring.

[Floris van Doorn]

Or is it false in that case?

[Reid Barton]

I think {0, 1}, 1 + 1 = 1 is a semiring

[Scott Morrison]

I've stuck with the proof via nonzero_comm_ring, https://github.com/leanprover-community/mathlib/pull/1540/files#diff-997c56fe87e1352880681d783e610a7f, just because it's more general (but not as general as possible, which would require adjusting the algebraic hierarchy for very little gain).