F : Type ?u.75707
α : Type u_1
β : Type ?u.75713
R : Type ?u.75716
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a b : α
⊢ a = b + b + 1 ↔ a = bit1 b
F : Type ?u.75707
α : Type u_1
β : Type ?u.75713
R : Type ?u.75716
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a b : α
⊢ a = 2 * b + 1 ↔ a = bit1 b
rw [two_mul]
no goals
F : Type ?u.75707
α : Type u_1
β : Type ?u.75713
R : Type ?u.75716
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a b : α
⊢ a = b + b + 1 ↔ a = bit1 b
rfl