Why can't linarith do simple association here?

Stream: general

[Sophia C]

So, I'm playing around with Lean, and I'm trying to prove a simple theorem:

{z : ℕ} : 4*z + (4 - 1) = (4*z + 4) - 1

and I can't seem to do it with linarith alone.

[Yury G. Kudryashov]

Short answer: try omega. Long answer: probably, linarith doesn't split nat subtraction into cases.

[Yury G. Kudryashov]

You can also try to zify and see if it can push Nat.cast (_ - _) to Nat.cast _ - Nat.cast _.

[Yury G. Kudryashov]

The issue is that (2 - 3 : Nat) = 0 in Lean/Mathlib, so a + (b - c) = (a + b) - c requires c ≤ b.

[James Sully]

that one's true by rfl