English
Let b be a Boolean and n a natural number. The numeral obtained by appending the bit b to n via the binary encoding is given by ofNat'(Nat.bit b n) = cond b Num.bit1 Num.bit0 (ofNat' n).
Русский
Пусть b — булево, n — натуральное. Число, соответствующее представлению в двоичной системе после добавления бита b к n, равняется cond b Num.bit1 Num.bit0 (ofNat' n).
LaTeX
$$$\\operatorname{ofNat'}\\left(\\operatorname{Nat}.\\text{bit}\\(b,n)\\right) = \\operatorname{cond}(b,\\operatorname{Num}.\\text{bit1},\\operatorname{Num}.\\text{bit0},\\operatorname{ofNat'}(n))$$$
Lean4
theorem ofNat'_bit (b n) : ofNat' (Nat.bit b n) = cond b Num.bit1 Num.bit0 (ofNat' n) :=
Nat.binaryRec_eq _ _ (.inl rfl)
