## Stream: general

### Topic: new nat lemmas (and naming)

#### Eric Wieser (Oct 22 2020 at 10:57):

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 (Oct 22 2020 at 10:58):

nat.add_sub_self_of_le and nat.sub_add_sub_cancel?

#### Eric Wieser (Oct 22 2020 at 11:00):

Those sound reasonable to me

(deleted)

#### Eric Wieser (Oct 22 2020 at 11:24):

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

#### Eric Wieser (Oct 22 2020 at 11:27):

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

#### Eric Wieser (Oct 22 2020 at 11:33):

#4738

Last updated: May 11 2021 at 00:31 UTC