Theorem: HTPI.neb_step (HTPILib/Chap8Part2.lean)

State before:
A : Set ℕ
n s : ℕ
⊢ num_elts_below A (n + 1) s ↔ n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1) ∨ n ∉ A ∧ num_elts_below A n s
Tactic:
rfl
State after:
no goals