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

State before:
a m : ℕ
⊢ a ∈ Set_rp_below m ↔ rel_prime m a ∧ a < m
Tactic:
rfl
State after:
no goals