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

State before:
i : ℤ
⊢ 1 < i → 0 < i
Tactic:
intro h
State after:
i : ℤ
h : 1 < i
⊢ 0 < i

State before:
i : ℤ
h : 1 < i
⊢ 0 < i
Tactic:
have hz : (0: ℤ) < 1 := by simp
State after:
i : ℤ
h : 1 < i
hz : 0 < 1
⊢ 0 < i

State before:
i : ℤ
h : 1 < i
hz : 0 < 1
⊢ 0 < i
Tactic:
apply lt_trans hz h
State after:
no goals

State before:
i : ℤ
h : 1 < i
⊢ 0 < 1
Tactic:
simp
State after:
no goals