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

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