Extend the theory of positive rationals `Qp`

This MR extends the theory of positive rationals Qp. The most important change is that it fixes the leaky abstraction, adds tons of lemmas, and no longer relies on the coercions to the non-negative rationals Qc to obtain notions like orders.

New features

• Add the orders Qc_le and Qp_lt.
• Add a function Qc_inv for the multiplicative inverse.
• Define the division function Qp_div in terms of Qp_inv, and generalize the second argument from positive to Qp.
• Define a function pos_to_Qp that converts a positive into a positive rational Qp.
• Add many lemmas and missing type class instances, especially for orders, multiplication, multiplicative inverse, division, and the conversion.

Technical changes:

• Remove the coercion from Qp to Qc. This follows our recent tradition of getting rid of coercions since they are more often confusing than useful.
• Rename the conversion from Qp to Qc from Qp_car into Qp_to_Qc to be consistent with other conversion functions in std++. Also rename the lemma Qp_eq into Qp_to_Qc_inj_iff.
• Use let '(..) = ... in the definitions of Qp_plus/Qp_mult/Qp_inv/Qp_le/Qp_lt to avoid Coq tactics (like injection) to unfold these definitions eagerly. We already used this trick in e.g., gmap for the same reason. This works around the Coq issue that @simonfv ran into here.
• Define the literals 1, 2, 3, 4 in terms of pos_to_Qp instead of iterated addition. This avoids weird rewrites. For example, before 2 was defined as 1 + 1, so rewriting with 1 = stuff in a goal containing 2 turned it into stuff + stuff, which was extremely confusing.

Things to discuss

• We could use Coq's extensible notation machinery to get proper notations for the literals. AFAIK this is only possible in Coq 8.9+, so that requires us to drop support for Coq 8.8. Do ▷
• While we are changing the API anyway, use add/mul instead of plus/mult, to be consistent with the lemmas for nat and Z.
• Also improve the Qc library in the same way. Do ▷

Impact on reverse dependencies

This MR will cause some breakage for libraries that rely on the order on fractions, but in my opinion, this is for the better. I have ported some of the developments that use fractions in interesting ways, namely Iris, Iron, and LambdaRust. While stuff broke, I managed to shorten proofs significantly by making use of the new lemmas introduced in this MR. Also, after this MR, none of these developments rely on the conversion to Qc anymore, showing that we indeed provide a reasonable API now.

Some stats:

• Iris: 66 insertions, 78 deletions
• LambdaRust: 32 insertions, 63 deletions
• Iron: no changes needed
• Examples: no changed needed, after removing an unused lemma
• gpfls: 8 insertions, 8 deletions

To land this MR, we should first merge iris!497 (merged).

theories/countable.v

@@ -269,11 +269,11 @@ Qed.
 
 Program Instance Qp_countable : Countable Qp :=
   inj_countable
-    Qp_car
+    Qp_to_Qc
     (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
 Next Obligation.
   intros [p Hp]. unfold mguard, option_guard; simpl.
-  case_match; [|done]. f_equal. by apply Qp_eq.
+  case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff.
 Qed.
 
 Program Instance fin_countable n : Countable (fin n) :=