Produce [1..n] in Coq

I'm reading Coq in a Hurry.
https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf
On page 8 there is the following exercise

Exercise on lists, map, and app. (app is like ++ in Haskell)
Define a function that takes as input a number n and returns a list with n elements, from 0 to n − 1.

I have written the following code.
Fixpoint ex2 (n : nat) :=
match n with
0 => (nil : list nat)
| S p => n :: ex2 p
end.
This produces the list in reverse order (nevermind it is [1..n], not [0..n-1]). Is there any functional way to produce a list in increasing order without using reverse? Keep in mind this is page 8 and I think I am not supposed to use auxiliary functions (or maybe I am?).

Definition dubs : nat -> Prop :=
fun n => exists x, exists y, n = x + 10*x + 100*y.

Theorem check_11 : dubs 11.
Proof.
unfold dubs.
exists 1; exists 0.
compute.
reflexivity.
Qed.

(* Nice dubs *)