Zulip Chat Archive

Stream: general

Topic: new nat lemmas (and naming)


view this post on Zulip 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]

view this post on Zulip Johan Commelin (Oct 22 2020 at 10:58):

nat.add_sub_self_of_le and nat.sub_add_sub_cancel?

view this post on Zulip Eric Wieser (Oct 22 2020 at 11:00):

Those sound reasonable to me

view this post on Zulip Gabriel Ebner (Oct 22 2020 at 11:19):

(deleted)

view this post on Zulip Eric Wieser (Oct 22 2020 at 11:24):

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

view this post on Zulip 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!

view this post on Zulip Eric Wieser (Oct 22 2020 at 11:33):

#4738


Last updated: May 11 2021 at 00:31 UTC