n✝ m n : ℕ
⊢ { val := n % (n + 1), isLt := (_ : n % (n + 1) < n + 1) } = { val := n, isLt := (_ : n < Nat.succ n) }
n✝ m n : ℕ
⊢ ↑n = last n
rw [← Fin.ofNat_eq_val, Fin.ofNat'', Fin.last]
no goals
n✝ m n : ℕ
⊢ { val := n % (n + 1), isLt := (_ : n % (n + 1) < n + 1) } = { val := n, isLt := (_ : n < Nat.succ n) }
simp only [Nat.mod_eq_of_lt n.lt_succ_self]