by_cases ha : a ≤ 0
a b : ℝ
hab : a ≤ b
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
case pos
a b : ℝ
hab : a ≤ b
ha : a ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

case neg
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting