rw [Finset.range_eq_Ico]
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p