case h.e'_3
α : Type u
β : Type ?u.61774
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a = 1 * a
α : Type u
β : Type ?u.61774
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a < b * a
convert mul_lt_mul_of_pos_right hm hn
no goals
case h.e'_3
α : Type u
β : Type ?u.61774
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a = 1 * a
rw [one_mul]