stupid inequality

Stream: new members

[Alex Kontorovich]

What's the tactic that kills stuff like this? (If $1 \le c < 1/2$ then false.)

import Mathlib

theorem extracted_1 (c : ℝ) (this_4 : 1 ≤ c) (this : c < 2⁻¹) : False := sorry
-- simp fails
-- linarith fails
-- exact? fails
-- apply? junk
-- rw? junk

I shouldn't have to look up some lt_of_le_of_lt kind of thing, right?... Thanks!

[David Renshaw]

This works:

 norm_num at this; linarith

[David Renshaw]

I wonder if linarith preprocessing ought to automatically do that kind of thing

[David Renshaw]

(Apparently linarith currently does not know what do with 2⁻¹.)