no goals
α : Type u_1
a b c d : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : 1 < a
⊢ b < a * b
simpa only [one_mul] using mul_lt_mul_of_pos_right h hb