α : Type u_1
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
h : 0 < c
⊢ 0 < b ↔ 0 * c < b
α : Type u_1
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
h : 0 < c
⊢ 0 < b * c ↔ 0 < b
rw [←zero_mul c, mul_lt_mul_right h]
no goals
α : Type u_1
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
h : 0 < c
⊢ 0 < b ↔ 0 * c < b
simp