mathlib version of `le_or_succ_le`

Stream: new members

[rzeta0]

I'm trying to find a lemma which splits the natural numbers as follows:

$$(n \le m) \lor (m+1 \le n) \text{ for } n,m \in \mathbb{N}$$

Heather MacBeth's course has a lemma

lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a :=

I've tried searching with Moogle and Loogle but can't find anything equivalent. I have searched for a lemma that follows the common naming convention and also using search terms

​n ≤ m ∨ succ m ≤ n

---

The reason I want such a lemma is to create a simple educational example around the following challenge, and I want to keep both the code simple and also the concepts simple (splitting the natural number line into two).

example {n : ℕ} : n^2 ≠ 2 := by
  -- have h := le_or_succ_le n 1

[rzeta0]

I have mentioned this lemma before in different questions but having searched I can't find an answer to this specific question. Apologies if I've duplicated.

[Ruben Van de Velde]

No opinion on whether it should be in mathlib, but it can be proved quite quickly:

import Mathlib.Data.Nat.Defs
lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.succ_le]
  exact le_or_lt a b

[Vincent Beffara]

It is in mathlib ;-)

import Mathlib.Data.Nat.Defs
lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a := le_or_lt a b

[Ruben Van de Velde]

That's naughty, though :)

[rzeta0]

@Ruben Van de Velde - sadly we haven't learned about square brackets nor exact yet

@Vincent Beffara I can't tell if your reply is in jest or not. I couldn't find it. Are you creating the lemma on the fly? That would be too much for the beginner examples I'm creating.

[rzeta0]

If it isn't in mathlib - because it is so useful for beginners, perhaps I should propose on the github that it should be?

[Ruben Van de Velde]

The lemma Vincent is using says a ≤ b ∨ b < a. It just so happens (and you should not rely on this) that b < a is defined as b + 1 ≤ a, so this actually matches the statement you're looking for

[rzeta0]

So is it the case there really isn't an equivalent to le_or_succ_le in mathlib?

If this is correct, I will stop searching, and try creating a different tutorial example entirely.

[Vincent Beffara]

Yes my reply was kind of a joke, the lemma you want certainly makes sense. You indeed should not rely on the definition of < on Nat, especially as a beginner.

I'm guessing that the reason it is not in mathlib while plenty of seemingly as simple lemmas are, is precisely because of the way < is defined here docs#Nat.lt (so le_or_lt for Nat really is identical as the lemma that you want).

[rzeta0]

@Vincent Beffara - so what is the best way to proceed, noting that I shouldn't rely on an internal definition of < on Nat?

The docs you point to say "The strict less than relation on natural numbers is defined as n < m := n + 1 ≤ m."

Is there a way to then use that definition of < to achieve what I want in a safe way?

---

The following is my attempy using simple lemmas and the result is ugly!

It should not requite the application of 4 lemmas!

import Mathlib.Tactic

example {n : ℕ} : n^2 ≠ 2 := by
  -- have h := le_or_succ_le n 1
  have h := le_or_lt n 1
  obtain ha | hb := h
  -- ha : n ≤ 1
  -- hb : 1 < n
  · apply ne_of_lt
    calc
      n^2 ≤ (1)^2 := by rel [ha]
      _ < 2 := by norm_num
  · apply ne_of_gt
    have h2 := Nat.succ_le_of_lt hb -- h2 : Nat.succ 1 ≤ n
    calc
      n^2 ≥ (2)^2 := by rel [h2]
      _ > 2 := by norm_num

[Damiano Testa]

In this case, there is good automation, so you do not have to remember/look up all the names:

example {n : ℕ} : n^2 ≠ 2 := by
  obtain _|_|n := n <;> ring_nf <;> omega

[rzeta0]

@Damiano Testa I've not come across omega in any course yet. Is it purely a tool for guessing suitable bridging lemmas?

[Damiano Testa]

It should have a doc-string, explaining what it does, but basically it solves linear goals in Nat/Int.

[Vincent Beffara]

Or without automation you could start like this distinguishing cases (which is essentially the first step in Damiano's code):

example {n : ℕ} : n^2 ≠ 2 := by
  match n with
  | 0 => norm_num
  | 1 => norm_num
  | k + 2 =>
    sorry

(Lean knows that a natural is either 0 or 1 or something+2)

[rzeta0]

I'm going to start a new question asking how to add a le_or_succ_le to mathlib.