Theorem: gt_zero_ne_zero (HOLFloat/Fixed_theroem.lean)

State before:
x : ℤ
⊢ 1 < x → x ≠ 0
Tactic:
intros h h₁
State after:
x : ℤ
h : 1 < x
h₁ : x = 0
⊢ False

State before:
x : ℤ
h : 1 < x
h₁ : x = 0
⊢ False
Tactic:
simp [h₁] at h
State after:
no goals