not equal from less than or greater than for reals

Stream: new members

[Thomas Preu]

I am trying to prove the statements from this thread as an exercise. I am stuck at proving not equal 0 ≠ a from less than 0 < a. That surely is a statement somewhere in Mathlib, I would be happy, if someone could point me to it.

[Robin Arnez]

for h : 0 < a, there's docs#ne_of_lt, or even shorter h.ne

[Thomas Preu]

Thank you, that did it. I wonder why I did not find it via a search engine.

[Ruben Van de Velde]

https://loogle.lean-lang.org/?q=%3Fa+%3C+%3Fb+%E2%86%92+%3Fa+%E2%89%A0+%3Fb finds these, and another 20 specialized variants. (The general ones are sadly last in the list)

[Aaron Liu]

Thomas Preu said:

Thank you, that did it. I wonder why I did not find it via a search engine.

what did you try

[Kevin Buzzard]

See https://leanprover-community.github.io/blog/posts/searching-for-theorems-in-mathlib/ for some good ways to search for Lean theorems.

[Thomas Preu]

Aaron Liu said:

Thomas Preu said:

Thank you, that did it. I wonder why I did not find it via a search engine.

what did you try

I used plain google with queries like "lean4 prove not equal from less than" and some variations of it. I was not aware there is a specialized search tool for it.