a > a is false

Stream: new members

[Debendro Mookerjee]

Is there any way to show that a > a is false in lean?

[Bryan Gin-ge Chen]

Here's one way:

import tactic

example (a : ℕ) : ¬ a < a := by library_search
-- Try this: exact irrefl a

example (a : ℕ) : ¬ a < a := irrefl a

[Daniel Keys]

Here's another:

lemma L1 (a : ℕ) : ¬ a > a :=
begin
    push_neg, apply le_iff_lt_or_eq.2, right, refl,
end

[Debendro Mookerjee]

Thanks appreciate it!