Best way to split this cases?

Stream: new members

[YH]

If a, b, c ≥ 0 and I want to split them as either all of them is 0 or at least one of them is > 0, what is the best way to do this?

[Kevin Buzzard]

I'd be tempted to first case on a=0 and then in the =0 case case on b=0 etc

[YH]

I realized I can do that. But then it will leave me with 7 cases where at least one of a, b, c is not zero, is there a way to somehow "unify" them? Or this is the best we can do.

[Reid Barton]

How do you want to use the statement "at least one of them is > 0"?

[YH]

Say m = a + b + c, if at least one of them is > 0 then we have m > 0. Maybe I'd better just split the cases on m.

[Johan Commelin]

So these are all nats?

[Johan Commelin]

You can do

by_cases habc : a = 0 \and b = 0 \and c = 0,
{ rcases habc with \< rfl, rfl, rfl \>, sorry },
{ push_neg at habc,
  sorry }