English
For every PosNum n, the natural value of pred' n equals Nat.pred n.
Русский
Пусть n — положительное число. Тогда (pred' n : ℕ) = Nat.pred n.
LaTeX
$$$ (pred' n : \mathbb{N}) = \mathrm{Nat.pred}(n) $$$
Lean4
theorem pred'_to_nat : ∀ n, (pred' n : ℕ) = Nat.pred n
| 1 => rfl
| bit0 n =>
have : Nat.succ ↑(pred' n) = ↑n := by rw [pred'_to_nat n, Nat.succ_pred_eq_of_pos (to_nat_pos n)]
match (motive := ∀ k : Num, Nat.succ ↑k = ↑n → ↑(Num.casesOn k 1 bit1 : PosNum) = Nat.pred (n + n)) pred' n,
this with
| 0, (h : ((1 : Num) : ℕ) = n) => by rw [← to_nat_inj.1 h]; rfl
| Num.pos p, (h : Nat.succ ↑p = n) => by rw [← h]; exact (Nat.succ_add p p).symm
| bit1 _ => rfl
