This fix is inspired by !198.

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.

These were very specific, there were no lemmas about them. They were used
back in the days for some specific things in my C semantics.

Fix in preparation for https://github.com/coq/coq/pull/13188

Thanks to @simongregersen for reporting.

Note that prior to 0d7a7f06 we would get this instance automatically,
but that instance would not have the right computational behavior.

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Set Default Goal Selector "!" makes it illegal to ever apply a tactic
with more than one goal (instead, must focus with bullets or braces).

Hugo Herbelin authored 4 years ago and Robbert Krebbers committed 4 years ago

This is a consequence of Coq PR #12950 which gives to import the
effect of reactivating the imported notations.