no goals
R : Type u
inst✝ : AddGroupWithOne R
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1
cases h
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑(n + 1) - 1
rw [cast_succ, add_sub_cancel]
no goals
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n
rfl