Theorem: Nat.pred_lt_iff (Lib.lean)

State before:
n : ℕ
⊢ n - 1 < n ↔ n ≠ 0
Tactic:
cases n <;> simp
State after:
no goals