add_tsub_add_le_tsub_add_tsub

Stream: Is there code for X?

[Andrew Yang]

Do we have this (or an easy proof of this) somewhere?

lemma add_tsub_add_le_tsub_add_tsub {a b c d : ℕ} :
  (a + b) - (c + d) ≤ (a - c) + (b - d) :=
begin
  cases le_total (a + b) (c + d) with h₁ h₁,
  { rw tsub_eq_zero_of_le h₁, exact zero_le _ },
  cases le_total (a) (c) with h₂ h₂,
  { rw [tsub_eq_zero_of_le h₂, zero_add, tsub_le_iff_tsub_le],
    exact add_tsub_le_assoc.trans (add_le_add h₂ tsub_tsub_le) },
  cases le_total (b) (d) with h₃ h₃,
  { rw [tsub_eq_zero_of_le h₃, add_zero, tsub_le_iff_tsub_le, add_comm a, add_comm c],
    exact add_tsub_le_assoc.trans (add_le_add h₃ tsub_tsub_le) },
  { simp only [← int.coe_nat_le_coe_nat_iff, nat.cast_sub, nat.cast_add, *], linarith }
end

[Yaël Dillies]

The equality is docs#tsub_add_tsub_comm

[Andrew Yang]

This is a proof with a more reasonable length

lemma add_tsub_add_le_tsub_add_tsub {a b c d : ℕ} :
  (a + b) - (c + d) ≤ (a - c) + (b - d) :=
begin
  rw [add_comm c, ← tsub_tsub],
  refine (tsub_le_tsub_right add_tsub_le_assoc c).trans _,
  rw [add_comm a, add_comm (a - c)],
  exact add_tsub_le_assoc
end

[Yaël Dillies]

@Andrew Yang, did you ever PR the above? If not, I am about to PR very similar lemmas so I'll include that one.

[Andrew Yang]

It is somewhere in #15105, but the right thing to do is probably to put this lemma in your PR and to make my PR depend on it.

[Andrew Yang]

@Yaël Dillies Did you end up PRing the lemma?

[Yaël Dillies]

I was working on it this morning. I can probably finish it up now.

[Andrew Yang]

I see. In this case, I think I will merge my PR containing it (#15459) first, so you can leave it out from your PR?

[Yaël Dillies]

@Andrew Yang, here you go: #15497