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

State before:
m a i : ℕ
⊢ [↑(G m a i)]_m = [↑a * ↑i % ↑m]_m
Tactic:
rfl
State after:
no goals