no goals
α : Type ?u.333835
n : PosNum
⊢ ↑(size (bit0 n)) = natSize (bit0 n)
rw [size, succ_to_nat, natSize, size_eq_natSize n]
no goals
α : Type ?u.333835
n : PosNum
⊢ ↑(size (bit1 n)) = natSize (bit1 n)
rw [size, succ_to_nat, natSize, size_eq_natSize n]