α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(PosNum.bit0 p) = _root_.bit0 ↑p
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(ZNum.bit0 (pos p)) = _root_.bit0 ↑(pos p)
rw [ZNum.bit0, cast_pos, cast_pos]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(PosNum.bit0 p) = _root_.bit0 ↑p
rfl
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(ZNum.bit0 (neg p)) = _root_.bit0 ↑(neg p)
rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, _root_.bit0, _root_.bit0, neg_add_rev]