Theorem about cancelling nat

Stream: Is there code for X?

[Bolton Bailey]

Do we have

import Mathlib.Algebra.Group.Basic
import Mathlib.Data.Nat.Basic

lemma foo (a b : ℕ) : a = a + b ↔ b = 0 := by exact self_eq_add_right

[Yaël Dillies]

In #11633, yes. Currently, no

[Yaël Dillies]

You should expect this to be stated as a + b = a ↔ b = 0

[Bolton Bailey]

Hmm, exact? in the web editor gives self_eq_add_right

[Yaël Dillies]

Ugh, I am bamboozled

[Bolton Bailey]

I guess I just don't have enough imports where I am currently working

[Kevin Buzzard]

you need to import NNG ;-)

[Bolton Bailey]

Hmm, even trickier than just importing since I need AddLeftCancelMonoid ℕ as well

[Bolton Bailey]

How do I find where that is defined?

[Yaël Dillies]

Data.Nat.Basic

[Yaël Dillies]

(I do not know the entire content of mathlib I swear :fingers_crossed:)

[Bolton Bailey]

No, why isn't the code above working then?

[Yaël Dillies]

Ah sorry, there should have been a shortcut instance but I guess it's currently derived from order cancellativity, so you instead need Data.Nat.Order.Basic