α : Type u
β : Type ?u.25897
inst✝¹ : OrderedSemiring α
a b c d : α
h : 0 < a
inst✝ : Nontrivial α
⊢ 0 < bit1 a
α : Type u
β : Type ?u.25897
inst✝ : OrderedSemiring α
a b c d : α
h : 0 < a
⊢ 0 < bit1 a
nontriviality
no goals
α : Type u
β : Type ?u.25897
inst✝¹ : OrderedSemiring α
a b c d : α
h : 0 < a
inst✝ : Nontrivial α
⊢ 0 < bit1 a
exact bit1_pos h.le