case splitting the wrong way

Stream: new members

[Lucas Allen]

Hello, I have the hypothesis k < nat.succ n, and I want to split the goal into two goals, one where the hypothesis is k < n and another where the hypothesis is k = n. This is a bit like cases but going the wrong direction. Is there some way to do this?

[Alex J. Best]

rw nat.lt_succ_iff_lt_or_eq at h,
cases h,

or cases nat.lt_succ_iff_lt_or_eq.mp h,

[Lucas Allen]

Ahh... Thanks.