English
For every positive number p, the embedding Num.ofNat' of (p as a natural) equals Num.pos p.
Русский
Для любого положительного числа p отображение Num.ofNat'(p) совпадает с Num.pos p.
LaTeX
$$$\\forall p \in \\text{PosNum}, \\operatorname{Num}.ofNat' (p : \\mathbb{N}) = \\operatorname{Num}.pos p$$$
Lean4
@[simp]
theorem of_to_nat' : ∀ n : PosNum, Num.ofNat' (n : ℕ) = Num.pos n
| 1 => by erw [@Num.ofNat'_bit true 0, Num.ofNat'_zero]; rfl
| bit0 p => by simpa only [Nat.bit_false, cond_false, two_mul, of_to_nat' p] using Num.ofNat'_bit false p
| bit1 p => by simpa only [Nat.bit_true, cond_true, two_mul, of_to_nat' p] using Num.ofNat'_bit true p
