⊢ cond true Num.bit1 Num.bit0 0 = Num.pos 1
⊢ Num.ofNat' ↑1 = Num.pos 1
erw [@Num.ofNat'_bit true 0, Num.ofNat'_zero]
no goals
⊢ cond true Num.bit1 Num.bit0 0 = Num.pos 1
rfl
p : PosNum
⊢ cond false Num.bit1 Num.bit0 (Num.pos p) = Num.pos (bit0 p)
p : PosNum
⊢ Num.ofNat' ↑(bit0 p) = Num.pos (bit0 p)
erw [@Num.ofNat'_bit false, of_to_nat' p]
no goals
p : PosNum
⊢ cond false Num.bit1 Num.bit0 (Num.pos p) = Num.pos (bit0 p)
rfl
p : PosNum
⊢ cond true Num.bit1 Num.bit0 (Num.pos p) = Num.pos (bit1 p)
p : PosNum
⊢ Num.ofNat' ↑(bit1 p) = Num.pos (bit1 p)
erw [@Num.ofNat'_bit true, of_to_nat' p]
no goals
p : PosNum
⊢ cond true Num.bit1 Num.bit0 (Num.pos p) = Num.pos (bit1 p)
rfl