Splitting to x=0 and x>0 cases when x>=0 is known

Stream: new members

[Michael Novak]

Hi,
I'm sure I've seen this before, but for some reason I struggle using h : x \ge 0 to split the proof to the case where x=0 and the case where x>0. I would really appreciate if someone could remind me of a good way of doing this.

[Etienne Marion]

obtain rfl | h := eq_or_lt_of_le’ h

[Michael Novak]

thank you very much!

[Kenny Lau]

@Michael Novak btw you should use b le a over a ge b

[Michael Novak]

Kenny Lau said:

Michael Novak btw you should use b le a over a ge b

You're right, thanks for the reminder!

[Jakub Nowak]

You might also be able to use match:

example (x : Int) (h : x ≥ 0) : False := by
  match x with
  | 0 => sorry
  | Int.ofNat (x + 1) => sorry

At least for Int, Lean is able to deduce that the Int.negSucc case is impossible. Although this doesn't give you x > 0 assumption directly.