n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
⊢ ↑(val ↑a) = a % ↑n
n : ℕ
a : ℤ
inst✝ : NeZero n
⊢ ↑(val ↑a) = a % ↑n
have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.coe_nat_nonneg _
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
hlt : ↑(val ↑a) < ↑n
⊢ ↑(val ↑a) = a % ↑n
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
⊢ ↑(val ↑a) = a % ↑n
have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
hlt : ↑(val ↑a) < ↑n
⊢ ↑(val ↑a) % ↑n = a % ↑n
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
hlt : ↑(val ↑a) < ↑n
⊢ ↑(val ↑a) = a % ↑n
refine' (Int.emod_eq_of_lt hle hlt).symm.trans _
no goals
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(val ↑a)
hlt : ↑(val ↑a) < ↑n
⊢ ↑(val ↑a) % ↑n = a % ↑n
rw [← ZMod.int_cast_eq_int_cast_iff', Int.cast_ofNat, ZMod.nat_cast_val, ZMod.cast_id]