Replace unused pattern variables with underscore

See merge request !203

Addresses new unused-pattern-matching-variable warning on Coq master.

Add explicit Global to hints at top level

See merge request iris/stdpp!202

Fixes new Coq master warning deprecated-hint-without-locality.

Set `Hint Mode` for `pretty`.

See merge request !201

Add lemmas about `list_to_map`

See merge request iris/stdpp!199

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

See merge request !200

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

This fix is inspired by iris/stdpp!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.