Formalizing a telescoping Sum of Prime gaps.

Stream: new members

[Kajani Kaunda]

Hello,
How would one formalize the following telescoping sum of prime gaps?

$$p_{m} - p_{n}=\sum_{k=n}^{m-1} (p_{k+1} - p_{k})$$

where the expression is valid for all n ≥ 1 and m > n and p is a prime number.

Regards,
Kajani

[Yaël Dillies]

docs#Finset.sum_range_sub is the closest we've got in mathlib

[Kajani Kaunda]

Yaël Dillies said:

docs#Finset.sum_range_sub is the closest we've got in mathlib

Ah, Ok will check it out thank you.

[Eric Wieser]

Can we do better than an Icc version for Nat, Int, PNat, ...?

[Eric Wieser]

Maybe one with Order.succ?