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

State before:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ a % m ∈ Set_rp_below m
Tactic:
define
State after:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m (a % m) ∧ a % m < m

State before:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m (a % m) ∧ a % m < m
Tactic:
rewrite [rel_prime_mod]
State after:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m a ∧ a % m < m

State before:
a m : ℕ
inst✝ : NeZero m
h1 : rel_prime m a
⊢ rel_prime m a ∧ a % m < m
Tactic:
show rel_prime m a ∧ a % m < m from
  And.intro h1 (mod_nonzero_lt a (NeZero.ne m))
State after:
no goals