Theorem: HTPI.I_def (HTPILib/Chap8Part1.lean)

State before:
k n : ℕ
⊢ k ∈ I n ↔ k < n
Tactic:
rfl
State after:
no goals