R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit0 a = bit0 b
⊢ a = b
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit1 a = bit1 b
⊢ a = b
simp only [bit1, add_left_inj] at h
no goals
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a b : R
h : bit0 a = bit0 b
⊢ a = b
exact bit0_injective h