by_cases and by_contradiction with inequalities

Stream: general

[Scott Morrison]

How would people feel about by_cases a ≤ b returning h : b < a in the second branch, rather than h : ¬(a ≤ b)?

I'm worried that there's not a really principled way to do this (do we just hack in something for inequalities?) (do we add a simp_set and apply that?) but it seems like to could make life smoother for most people.

[Kenny Lau]

by_cases! will perform by_cases and push_neg

[Kenny Lau]

(just like contrapose!)

[Scott Morrison]

Where is by_cases! implemented? Hitting F12 takes me to by_cases, with no sign of parsing for a !

[Scott Morrison]

I can't find any usage at all of by_cases!.

[Kenny Lau]

by "will" I mean "I propose that"

[Scott Morrison]

oh

[Scott Morrison]

Sounds good.

[Kevin Buzzard]

Sounds great. Would be nice to have = and \ne as well