. rw [← Finset.filter_union]
  rw [Finset.Ico_union_Ico_eq_Ico (Nat.zero_le a.succ) (Nat.succ_le_succ ha)]
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x

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)))
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)))