## Stream: new members

### Topic: Best way to split this cases?

#### YH (Dec 13 2019 at 22:11):

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 (Dec 13 2019 at 22:39):

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

#### YH (Dec 13 2019 at 22:51):

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 (Dec 13 2019 at 22:52):

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

#### YH (Dec 13 2019 at 22:57):

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 (Dec 14 2019 at 05:28):

So these are all nats?

#### Johan Commelin (Dec 14 2019 at 05:31):

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 }


Last updated: May 13 2021 at 05:21 UTC