n✝ m n : ℕ
inst✝ : NeZero n
a : ℕ
h : a < n
⊢ ↑(ofNat'' a) = a
n✝ m n : ℕ
inst✝ : NeZero n
a : ℕ
h : a < n
⊢ ↑↑a = a
rw [← ofNat_eq_val]
no goals
n✝ m n : ℕ
inst✝ : NeZero n
a : ℕ
h : a < n
⊢ ↑(ofNat'' a) = a
exact Nat.mod_eq_of_lt h