new nat lemmas (and naming)

Stream: general

[Eric Wieser]

Are these simple enough to belong in mathlib? Can anyone suggest names?

lemma nat.what {a b : ℕ} (h : b ≤ a) : b + (a - b) = a :=
by rw [←nat.add_sub_assoc h, nat.add_sub_cancel_left]

lemma nat.what {a b c: ℕ} (hab : b ≤ a) (hbc : c ≤ b) : (a - b) + (b - c) = a - c :=
by rw [←nat.add_sub_assoc hbc, ←nat.sub_add_comm hab, nat.add_sub_cancel]

[Johan Commelin]

nat.add_sub_self_of_le and nat.sub_add_sub_cancel?

[Eric Wieser]

Those sound reasonable to me

[Gabriel Ebner]

(deleted)

[Eric Wieser]

The first lemma exists already as docs#nat.add_sub_cancel'

[Eric Wieser]

And docs#sub_add_sub_cancel exists for general additive groups, so clearly the name is correct. Thanks @Johan Commelin!

[Eric Wieser]

#4738