α : Type u_1
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < c
⊢ 0 < b ↔ c * 0 < b
α : Type u_1
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < c
⊢ 0 < c * b ↔ 0 < b
rw [←mul_zero c, mul_lt_mul_left h]
no goals
α : Type u_1
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
h : 0 < c
⊢ 0 < b ↔ c * 0 < b
simp