I have just started getting acquainted with Coq and I would like to write this sum on it:

\sum_{p=1}^{n} \frac{\mathrm{d}^p}{\mathrm{d}x^p} f(x)

This is what I have tried:

```
Require Import Coquelicot.Coquelicot.
Require Import Coq.Sets.Finite_sets.
Require Import Coq.Reals.Reals.
Section test.
Local Open Scope R_scope.
Variable f : R -> R.
Definition f_p (m : nat)(x : R) := Derive_n f m x.
Local Open Scope nat_scope.
Definition summation_range (n : nat) := sum (fin_range n)(fun p => (Derive_n p f)).
```

The `summation_range`

definition yields an error â€śThe reference fin_range was not found

in the current environmentâ€ť. Even though I have just imported the package `Require Import Coq.Sets.Finite_sets.`

, which should have `fin_range`

on it (according to ChatGPT).

What is the proper way to write it?