no goals
α : Type ?u.330131
n : PosNum
⊢ ↑(size (bit0 n)) = Nat.size ↑(bit0 n)
rw [size, succ_to_nat, size_to_nat n, cast_bit0, Nat.size_bit0 <| ne_of_gt <| to_nat_pos n]
no goals
α : Type ?u.330131
n : PosNum
⊢ ↑(size (bit1 n)) = Nat.size ↑(bit1 n)
rw [size, succ_to_nat, size_to_nat n, cast_bit1, Nat.size_bit1]