Theorem: HTPI.num_rp_below_base (HTPILib/Chap7.lean)

State before:
m : ℕ
⊢ num_rp_below m 0 = 0
Tactic:
rfl
State after:
no goals