nat lemmas

Stream: new members

[Scott Morrison]

Could anyone help me with an apparently easy lemma:

lemma sub_add_eq_add_sub_of_le {a b c : ℕ} (h : b ≤ a) : (a - b) + c = (a + c) - b :=
by omega -- overkill!

[Reid Barton]

lemma sub_add_eq_add_sub_of_le {a b c : ℕ} (h : b ≤ a) : (a - b) + c = (a + c) - b :=
begin
  symmetry,
  apply nat.sub_eq_of_eq_add,
  rw [←add_assoc, nat.add_sub_cancel' h],
end

[Reid Barton]

Seems like a candidate for addition to the library

[Mario Carneiro]

lemma sub_add_eq_add_sub_of_le {a b c : ℕ} (h : b ≤ a) : (a - b) + c = (a + c) - b :=
by rw [add_comm a, nat.add_sub_assoc h, add_comm]

I suggest the name nat.sub_add_eq_add_sub

[Scott Morrison]

Thanks!

[Scott Morrison]

I have a bunch more lemmas about nat (mostly about divisibility) that I would like to have in mathlib.

[Scott Morrison]

They are all proved, but I don't doubt my proofs are highly golfable.

[Scott Morrison]

(and maybe some are in the library, just library_search and I failed to find them)

[Scott Morrison]

What is the best way to proceed?

[Scott Morrison]

Should I just make a PR with all the lemmas, with my proofs?

[Scott Morrison]

Or should I post just the statements here for someone to give a thumbs-up or thumbs-down to each?

[Scott Morrison]

Or post the proofs here too?

[Mario Carneiro]

post a PR, we can suggest improvements in the review comments if necessary

[Mario Carneiro]

you are more likely to get an individual proof golfed if you post here, but don't overdo it