Mechanics of Proof 2.5

Stream: new members

[Don Burgess]

I am stuck on Exercise 8. Could anyone give me a clue or insight on how to procee?

Do I have the right idea?

How do I show: a=b=c=0?

Thanks for your help.

example {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b)
    (ha' : 0 ≤ a) (hb' : 0 ≤ b) (hc' : 0 ≤ c) :
    ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by
  use 0, 0, 0
  constructor
  . extra
  . constructor
    . extra
    . constructor
      . extra
      . constructor
        ring
        apply le_antisymm
        calc
          a ≤ b + c := by apply ha
          _ = 0 + 0 := by sorry

[Ruben Van de Velde]

Why did you start with use 0, 0, 0? Is that supposed to be the correct mathematical solution?

[Don Burgess]

I think x,y,z = 0 works, but I do not know how to prove it

[Alex J. Best]

Maybe you can start by considering the case where a = b = c = 1, this satisfies the hypotheses, but then a = y + z won't work with y = z = 0

[Ruben Van de Velde]

Also, ha', hb' and hc' are not needed