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.Ico (Nat.succ a) (Nat.succ b)), x
no goals