Theorem: Int.one_lt_ne_one (HOLFloat/Common.lean)

State before:
a : ℤ
h : 1 < a
⊢ a ≠ 1
Tactic:
intro a_1
State after:
a : ℤ
h : 1 < a
a_1 : a = 1
⊢ False

State before:
a : ℤ
h : 1 < a
a_1 : a = 1
⊢ False
Tactic:
simp_all only [one_lt_zero_le_iff, ne_eq]
State after:
no goals