no goals
α : Type ?u.217228
β : Type ?u.217231
γ : Type ?u.217234
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
⊢ a ≠ 0 → b ≠ 0 → a * b ≠ 0
simpa only [Ordinal.pos_iff_ne_zero] using mul_pos