1. 1
2. 2
3. 3
4. 4
5. 5
6. 6

import Mathlib

-- This is how you benchmark stuff I think
#count_heartbeats in
example {a b : ℝ} (hab : a * b ≤ 0) (ha : a ≠ 0) (hb : b ≠ 0) : (0 < a ∧ b < 0) ∨ (a < 0 ∧ 0 < b) := by
  grind [mul_nonpos_iff_neg_imp_nonneg.mp hab]