le_pred_of_lt for WithBot ℕ

Stream: Is there code for X?

[Daniel Weber]

Is there a nicer way to prove this?

import Mathlib

example (a : WithBot ℕ) (b : ℕ) (h : a < b) : a ≤ (b - 1 : ℕ) := by
  cases a
  case bot => simp
  case coe a =>
    rw [← WithBot.coe_natCast, WithBot.coe_le_coe, Nat.cast_id]
    rw [← WithBot.coe_natCast, WithBot.coe_lt_coe, Nat.cast_id] at h
    omega

[Kim Morrison]

You should add the missing simp lemma that (a : WithBot Nat) <= (b : WithBot Nat) iff a <= b to Mathlib.

[Daniel Weber]

I think a better lemma to add might be (a : WithBot Nat) = some a, and then it's just coe_le_coe

[Eric Wieser]

That wouldn't help with WithBot Real

[Eric Wieser]

Kim Morrison said a less general version of:

You should add the missing simp lemma that (a : WithBot A) <= (b : WithBot A) iff a <= b, for a b : Nat, to Mathlib.

I guess there are quite a lot of these to add: Bot/Top, le/lt, special case where one or both of a and b are 0/1/ofNat, intCast versions of the same, lemmas with intCast on one side and natCast on the other, ...

[Kim Morrison]

(To clarify, Eric doesn't mean that you shouldn't add this simp lemma, but that it should be more general that for Nat.)

[Eric Wieser]

I actually misread your suggestion as being the general one, and meant that Daniel's lemma probably isn't useful in the presence of (my reading of) yours