no goals
α : Type ?u.215952
β : Type ?u.215955
γ : Type ?u.215958
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h₁ : 0 < a
h₂ : 0 < b
⊢ 0 < a * b
simpa only [mul_zero] using mul_lt_mul_of_pos_left h₂ h₁