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

State before:
i j : ℤ
⊢ j < i ↔ j + 1 ≤ i
Tactic:
apply Iff.intro
State after:
case mp
i j : ℤ
⊢ j < i → j + 1 ≤ i

case mpr
i j : ℤ
⊢ j + 1 ≤ i → j < i