α : Type ?u.845967
n : PosNum
⊢ ↑(↑(pred' n) + 1) = ↑↑(pred' n) + 1
α : Type ?u.845967
n : PosNum
⊢ ↑n = ↑↑(pred' n) + 1
rw [← n.to_nat_to_int, to_nat_eq_succ_pred]
no goals
α : Type ?u.845967
n : PosNum
⊢ ↑(↑(pred' n) + 1) = ↑↑(pred' n) + 1
rfl