case mp
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = val z + p * k

case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = val z + p * k) → ↑n = z
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = val z + p * k
constructor
case mp
p n : ℕ
inst✝ : NeZero p
⊢ ∃ k, n = val ↑n + p * k
case mp
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = val z + p * k
rintro rfl
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = val ↑n + p * (n / p)
case mp
p n : ℕ
inst✝ : NeZero p
⊢ ∃ k, n = val ↑n + p * k
refine' ⟨n / p, _⟩
no goals
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = val ↑n + p * (n / p)
rw [val_nat_cast, Nat.mod_add_div]
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ ↑(val z + p * k) = z
case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = val z + p * k) → ↑n = z
rintro ⟨k, rfl⟩
no goals
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ ↑(val z + p * k) = z
rw [Nat.cast_add, nat_cast_zmod_val, Nat.cast_mul, nat_cast_self, MulZeroClass.zero_mul,
  add_zero]