Set `Hint Mode` for `pretty`.

See merge request !201

Add lemmas about `list_to_map`

See merge request !199

Pretty-print 0 as "0" for N, Z, and nat

See merge request !200

This is a copy/paste of the CHANGELOG in !198.

This fix is inspired by !198.

Extend the theory of positive rationals `Qp`

See merge request !188

Moreover, and suitable lemmas.

This follows the standard naming for Coq numbers, and avoids one using
the old lemma to break abstraction accidentally.

- Remove the coercion from `Qp` to `Qc`, and remove it into from `Qp_car` into
  `Qp_to_Qc` to be consistent with other conversion functions.
- Use `let '(..) = ...` in the definitions of `Qp_plus`/`Qp_mult`/`Qp_div` to
  avoid Coq tactics (like `injection`) to unfold these definitions eagerly.
- Define orders `Qp_le` and `Qp_lt`, instead of relying on the orders on `Qc`,
  which were obtained through the removed coercion into `Qc`.
- Lift lemmas about the orders from `Qc` to `Qp`.
- Improve variable names and use of notation scopes.

add a function to obtain a set with all elements of a finite type

See merge request !196