no goals
a b : Int
h : a * b = 0
⊢ a = 0 ∨ b = 0
exact match Int.lt_trichotomy a 0, Int.lt_trichotomy b 0 with
| .inr (.inl heq₁), _ => .inl heq₁
| _, .inr (.inl heq₂) => .inr heq₂
| .inl hlt₁, .inl hlt₂ => absurd h <| Int.ne_of_gt <| Int.mul_pos_of_neg_of_neg hlt₁ hlt₂
| .inl hlt₁, .inr (.inr hgt₂) => absurd h <| Int.ne_of_lt <| Int.mul_neg_of_neg_of_pos hlt₁ hgt₂
| .inr (.inr hgt₁), .inl hlt₂ => absurd h <| Int.ne_of_lt <| Int.mul_neg_of_pos_of_neg hgt₁ hlt₂
| .inr (.inr hgt₁), .inr (.inr hgt₂) => absurd h <| Int.ne_of_gt <| Int.mul_pos hgt₁ hgt₂