case zero
a : ℕ
⊢ val ↑a = a % Nat.zero

case succ
a n✝ : ℕ
⊢ val ↑a = a % Nat.succ n✝
n a : ℕ
⊢ val ↑a = a % n
cases n
case succ
a n✝ : ℕ
⊢ val (Fin.ofNat'' a) = a % Nat.succ n✝
case succ
a n✝ : ℕ
⊢ val ↑a = a % Nat.succ n✝
rw [← Fin.ofNat_eq_val]
no goals
case succ
a n✝ : ℕ
⊢ val (Fin.ofNat'' a) = a % Nat.succ n✝
rfl
case zero
a : ℕ
⊢ val ↑a = a
case zero
a : ℕ
⊢ val ↑a = a % Nat.zero
rw [Nat.mod_zero]
no goals
case zero
a : ℕ
⊢ val ↑a = a
exact Int.natAbs_ofNat a