Zify and subtraction

Stream: Is there code for X?

[Terence Tao]

Is this lemma already in Mathlib? It was annoying to prove, and zify was only mildly helpful.

import Mathlib

lemma coe_of_sub_of_nat_eq (a b: ℕ) : (a-b:ℕ) = max (a-b:ℤ) 0 := by
  rcases le_or_lt b a with h | h
  . zify [h]
    apply (max_eq_left (sub_nonneg.mpr _)).symm
    norm_cast
  simp [Nat.sub_eq_zero_of_le (Nat.le_of_lt h)]
  apply (max_eq_right (sub_nonpos.mpr _)).symm
  norm_cast
  exact Nat.le_of_lt h

Related to this - would it make sense to make this lemma a zify_simps lemma, to be used when the simpler zify_simps lemmas docs#Mathlib.Tactic.Zify.Nat.cast_sub_of_add_le and docs#Nat.cast_sub_of_lt are not available? I find it much easier to manipulate the max (a-b:ℤ) 0 expression than the (a-b:ℕ) expression.

EDIT: similar questions could be raised for

lemma coe_of_int_toNat_eq (a:ℤ) : Int.toNat a = max 0 a := by
  rcases le_or_lt 0 a with h | h
  . rcases Int.eq_ofNat_of_zero_le h with ⟨n, rfl⟩
    simp
  simp [Int.toNat_eq_zero.mpr (le_of_lt h), (le_of_lt h)]

[Yury G. Kudryashov]

@loogle Nat.cast (Int.toNat _), max

[loogle]

:exclamation: unknown identifier 'max'
Did you mean Nat.cast (Int.toNat _), "max", Nat.cast (Int.toNat _), Max.max, or something else?

[Yury G. Kudryashov]

@loogle Nat.cast (Int.toNat _), Max.max

[loogle]

:search: Int.toNat_eq_max

[Yury G. Kudryashov]

It looks like the first lemma does not exist in the library.

[Alex J. Best]

Another proof using the omega tactic to avoid doing any heavy lifting

import Mathlib

lemma coe_of_sub_of_nat_eq (a b: ℕ) : (a-b:ℕ) = max (a-b:ℤ) 0 := by
  rw [max_def]
  split <;>
  omega