## Stream: general

### Topic: some lemmas

#### Scott Morrison (Oct 12 2019 at 10:17):

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 (Oct 12 2019 at 10:24):

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

#### Johan Commelin (Oct 12 2019 at 10:26):

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

#### Scott Morrison (Oct 12 2019 at 10:28):

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

#### Scott Morrison (Oct 12 2019 at 10:29):

example : zero_ne_one_class ℤ := infer_instance


#### Johan Commelin (Oct 12 2019 at 10:31):

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

#### Scott Morrison (Oct 12 2019 at 10:33):

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

#### Johan Commelin (Oct 12 2019 at 10:33):

I think you than have two incompatible zeros?

And two ones...

... yes.

#### Scott Morrison (Oct 12 2019 at 10:46):

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 (Oct 12 2019 at 11:57):

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 (Oct 12 2019 at 17:53):

The first one should be done for a nonzero_comm_semiring.

#### Floris van Doorn (Oct 12 2019 at 17:57):

Or is it false in that case?

#### Reid Barton (Oct 12 2019 at 17:59):

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

#### Scott Morrison (Oct 13 2019 at 06:41):

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).

Last updated: May 14 2021 at 06:16 UTC