no goals
R : Type u_1
A : Type ?u.107570
inst✝¹ : AddCommGroup R
inst✝ : StarAddMonoid R
x : R
hx : x ∈ skewAdjoint R
⊢ bit0 x ∈ skewAdjoint R
rw [mem_iff, star_bit0, mem_iff.mp hx, bit0, bit0, neg_add]