- 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.