α : Type ?u.462274
p : PosNum
⊢ Nat.pred ↑p = Nat.pred ↑(pos p)
α : Type ?u.462274
p : PosNum
⊢ ↑(pred (pos p)) = Nat.pred ↑(pos p)
rw [pred, PosNum.pred'_to_nat]
no goals
α : Type ?u.462274
p : PosNum
⊢ Nat.pred ↑p = Nat.pred ↑(pos p)
rfl