apply Finset.disjoint_filter_filter
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
case a
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.Ico 0 (Nat.succ a)) (Finset.Ico (Nat.succ a) (Nat.succ b))