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

State before:
m a : ℕ
inst✝ : NeZero m
⊢ maps_below m (G m a)
Tactic:
define
State after:
m a : ℕ
inst✝ : NeZero m
⊢ ∀ i < m, G m a i < m

State before:
m a : ℕ
inst✝ : NeZero m
⊢ ∀ i < m, G m a i < m
Tactic:
fix i : Nat
State after:
m a : ℕ
inst✝ : NeZero m
i : ℕ
⊢ i < m → G m a i < m

State before:
m a : ℕ
inst✝ : NeZero m
i : ℕ
⊢ i < m → G m a i < m
Tactic:
assume h1 : i < m
State after:
m a : ℕ
inst✝ : NeZero m
i : ℕ
h1 : i < m
⊢ G m a i < m

State before:
m a : ℕ
inst✝ : NeZero m
i : ℕ
h1 : i < m
⊢ G m a i < m
Tactic:
rewrite [G_def]
State after:
m a : ℕ
inst✝ : NeZero m
i : ℕ
h1 : i < m
⊢ a * i % m < m

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