Help with `example (a b : ℕ) (h : a ≥ b) : b = a - (a - b)`

Stream: new members

[ShatteredLead]

example (a b : ℕ) (h : a ≥ b) : b = a - (a - b) := by
  -- ?

rw [sub_sub_cancel] is not viable since it's only for AddCommGroups
And i have tried induction with b, with a, split a case for b, rewrite - with max, and all of them don't work.

But when we already know a ≥ b it should also be appropriate for natural numbers.
What's the easiest path to find out the proof? Thanks a lot!

[Yaël Dillies]

You want to use docs#tsub_tsub_cancel_of_le

[ShatteredLead]

Yaël Dillies said:

You want to use docs#tsub_tsub_cancel_of_le

Oh it works! Thank you!

[Kevin Buzzard]

You can answer questions like this yourself with

import Mathlib

example (a b : ℕ) (h : a ≥ b) : b = a - (a - b) := by
  exact?

A lot of basic claims like this are already in the library, and exact? searches to see if what you want is there.

Another approach is

import Mathlib

example (a b : ℕ) (h : a ≥ b) : b = a - (a - b) := by
  omega

i.e. try the general Nat tactics.