diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3dded487ae5a04cd656bb4ef53bff03af74792db..d4f13b19ebb7d9ae454cf8afcc0095a46754e3ed 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,12 +15,36 @@ Coq 8.8 and 8.9 are no longer supported.
   `zip_with` and `Forall2` versions of `∪`, `∖`, and `##`.
 - Remove unused type classes `DisjointE`, `DisjointList`, `LookupE`, and
   `InsertE`.
+- Overhaul of the theory of positive rationals `Qp`:
+  + Add the orders `Qp_le` and `Qp_lt`.
+  + Rename `Qp_plus` into `Qp_add` and `Qp_mult` into `Qp_mul` to be consistent
+    with the corresponding names for `nat`, `N`, and `Z`.
+  + Add a function `Qp_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`.
+  + Add 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.
+  + 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_car : Qp → Qc` 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` and `Qp_lt` to avoid Coq tactics (like `injection`) to unfold these
+    definitions eagerly.
+  + Define the `Qp` literals 1, 2, 3, 4 in terms of `pos_to_Qp` instead of
+    iterated addition.
+  + Rename and restate many lemmas so as to be consistent with the conventions
+    for Coq's number types `nat`, `N`, and `Z`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
 ```
 sed -i '
-s/\bQp_not_plus_q_ge_1\b/Qp_not_plus_ge/g
+s/\bQp_plus/Qp_add/g
+s/\bQp_mult/Qp_mul/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/countable.v b/theories/countable.v
index d837e7d543937e9a7acc8d63ea53a8bab2c3f8b7..2c07d66bcb93bc1ad91a0e96b9d9debb6be95b87 100644
--- a/theories/countable.v
+++ b/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) :=
diff --git a/theories/numbers.v b/theories/numbers.v
index 420c82d4870eb717d4ec36701339f88c1e7bcecf..ed42de032fef46f7db6652e78b06303c6676a057 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -627,6 +627,12 @@ Proof.
   by apply Qcmult_le_mono_nonneg_r.
 Qed.
 
+Lemma Qcinv_pos x : 0 < x → 0 < /x.
+Proof.
+  intros. assert (0 ≠ x) by (by apply Qclt_not_eq).
+  by rewrite (Qcmult_lt_mono_pos_r _ _ x), Qcmult_0_l, Qcmult_inv_l by done.
+Qed.
+
 Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n.
 Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed.
 Coercion Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n).
@@ -661,310 +667,524 @@ Local Close Scope Qc_scope.
 Declare Scope Qp_scope.
 Delimit Scope Qp_scope with Qp.
 
-(** The theory of positive rationals is very incomplete. We merely provide
-some operations and theorems that are relevant for fractional permissions. *)
-Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
-Hint Resolve Qp_prf : core.
-Arguments Qp_car _%Qp : assert.
+Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }.
+Add Printing Constructor Qp.
 Bind Scope Qp_scope with Qp.
+Arguments Qp_to_Qc _%Qp : assert.
 
-Local Open Scope Qc_scope.
 Local Open Scope Qp_scope.
 
-Definition Qp_one : Qp := mk_Qp 1 eq_refl.
-Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _.
-Next Obligation. by intros x y; apply Qcplus_pos_pos. Qed.
-Definition Qp_minus (x y : Qp) : option Qp :=
-  let z := (x - y)%Qc in
-  match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end.
-Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _.
-Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed.
+Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q.
+Proof.
+  split; [|by intros ->].
+  destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
+Qed.
+Instance Qp_eq_dec : EqDecision Qp.
+Proof.
+  refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
+    by rewrite <-Qp_to_Qc_inj_iff.
+Defined.
+
+Definition Qp_add (p q : Qp) : Qp :=
+  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
+  mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq).
+Arguments Qp_add : simpl never.
+
+Definition Qp_sub (p q : Qp) : option Qp :=
+  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
+  let pq := (p - q)%Qc in
+  guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq).
+Arguments Qp_sub : simpl never.
+
+Definition Qp_mul (p q : Qp) : Qp :=
+  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
+  mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq).
+Arguments Qp_mul : simpl never.
+
+Definition Qp_inv (q : Qp) : Qp :=
+  let 'mk_Qp q Hq := q return _ in
+  mk_Qp (/ q)%Qc (Qcinv_pos _ Hq).
+Arguments Qp_inv : simpl never.
+
+Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q).
+Typeclasses Opaque Qp_div.
+Arguments Qp_div : simpl never.
+
+Infix "+" := Qp_add : Qp_scope.
+Infix "-" := Qp_sub : Qp_scope.
+Infix "*" := Qp_mul : Qp_scope.
+Notation "/ q" := (Qp_inv q) : Qp_scope.
+Infix "/" := Qp_div : Qp_scope.
+
+Program Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Z.pos n) _.
+Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed.
+Arguments pos_to_Qp : simpl never.
 
-Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
-Next Obligation.
-  intros x y. unfold Qcdiv. assert (0 < Zpos y)%Qc.
-  { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
-  by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
-    <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
+Notation "1" := (pos_to_Qp 1) : Qp_scope.
+Notation "2" := (pos_to_Qp 2) : Qp_scope.
+Notation "3" := (pos_to_Qp 3) : Qp_scope.
+Notation "4" := (pos_to_Qp 4) : Qp_scope.
+
+Definition Qp_le (p q : Qp) : Prop :=
+  let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p ≤ q)%Qc.
+Definition Qp_lt (p q : Qp) : Prop :=
+  let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p < q)%Qc.
+
+Infix "≤" := Qp_le : Qp_scope.
+Infix "<" := Qp_lt : Qp_scope.
+Notation "p ≤ q ≤ r" := (p ≤ q ∧ q ≤ r) : Qp_scope.
+Notation "p ≤ q < r" := (p ≤ q ∧ q < r) : Qp_scope.
+Notation "p < q < r" := (p < q ∧ q < r) : Qp_scope.
+Notation "p < q ≤ r" := (p < q ∧ q ≤ r) : Qp_scope.
+Notation "p ≤ q ≤ r ≤ r'" := (p ≤ q ∧ q ≤ r ∧ r ≤ r') : Qp_scope.
+Notation "(≤)" := Qp_le (only parsing) : Qp_scope.
+Notation "(<)" := Qp_lt (only parsing) : Qp_scope.
+
+Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core.
+
+Lemma Qp_to_Qc_inj_le p q : p ≤ q ↔ (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc.
+Proof. by destruct p, q. Qed.
+Lemma Qp_to_Qc_inj_lt p q : p < q ↔ (Qp_to_Qc p < Qp_to_Qc q)%Qc.
+Proof. by destruct p, q. Qed.
+
+Instance Qp_le_dec : RelDecision (≤).
+Proof.
+  refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
+    by rewrite Qp_to_Qc_inj_le.
 Qed.
+Instance Qp_lt_dec : RelDecision (<).
+Proof.
+  refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
+    by rewrite Qp_to_Qc_inj_lt.
+Qed.
+Instance Qp_lt_pi p q : ProofIrrel (p < q).
+Proof. destruct p, q; apply _. Qed.
 
 Definition Qp_max (q p : Qp) : Qp := if decide (q ≤ p) then p else q.
 Definition Qp_min (q p : Qp) : Qp := if decide (q ≤ p) then q else p.
 
-Infix "+" := Qp_plus : Qp_scope.
-Infix "-" := Qp_minus : Qp_scope.
-Infix "*" := Qp_mult : Qp_scope.
-Infix "/" := Qp_div : Qp_scope.
-Infix "`max`" := Qp_max (at level 35) : Qp_scope.
-Infix "`min`" := Qp_min (at level 35) : Qp_scope.
-Notation "1" := Qp_one : Qp_scope.
-Notation "2" := (1 + 1)%Qp : Qp_scope.
-Notation "3" := (1 + 2)%Qp : Qp_scope.
-Notation "4" := (1 + 3)%Qp : Qp_scope.
+Infix "`max`" := Qp_max : Qp_scope.
+Infix "`min`" := Qp_min : Qp_scope.
 
-Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y.
+Instance Qp_inhabited : Inhabited Qp := populate 1.
+
+Instance Qp_add_assoc : Assoc (=) Qp_add.
+Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed.
+Instance Qp_add_comm : Comm (=) Qp_add.
+Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcplus_comm. Qed.
+Instance Qp_add_inj_r p : Inj (=) (=) (Qp_add p).
 Proof.
-  split; [by intros ->|].
-  destruct x, y; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
+  destruct p as [p ?].
+  intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (Qcplus p)).
 Qed.
-
-Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
-Instance Qp_eq_dec : EqDecision Qp.
+Instance Qp_add_inj_l p : Inj (=) (=) (λ q, q + p).
 Proof.
- refine (λ x y, cast_if (decide (Qp_car x = Qp_car y))); by rewrite Qp_eq.
-Defined.
-
-Instance Qp_plus_assoc : Assoc (=) Qp_plus.
-Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
-Instance Qp_plus_comm : Comm (=) Qp_plus.
-Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.
-Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
-Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). Qed.
-Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp.
-Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed.
+  destruct p as [p ?].
+  intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc).
+Qed.
 
-Lemma Qp_minus_diag x : (x - x)%Qp = None.
-Proof. unfold Qp_minus, Qcminus. by rewrite Qcplus_opp_r. Qed.
-Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y.
+Instance Qp_mul_assoc : Assoc (=) Qp_mul.
+Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed.
+Instance Qp_mul_comm : Comm (=) Qp_mul.
+Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed.
+Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p).
 Proof.
-  unfold Qp_minus, Qcminus; simpl.
-  rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r.
-  destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq.
+  destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl.
+  intros Hpq.
+  apply (anti_symm _); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
 Qed.
+Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p).
+Proof.
+  intros q1 q2 Hpq. apply (inj (Qp_mul p)). by rewrite !(comm_L Qp_mul p).
+Qed.
+
+Lemma Qp_mul_add_distr_l p q r : p * (q + r) = p * q + p * r.
+Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_r. Qed.
+Lemma Qp_mul_add_distr_r p q r : (p + q) * r = p * r + q * r.
+Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_l. Qed.
+Lemma Qp_mul_1_l p : 1 * p = p.
+Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed.
+Lemma Qp_mul_1_r p : p * 1 = p.
+Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed.
 
-Instance Qp_mult_assoc : Assoc (=) Qp_mult.
-Proof. intros x y z; apply Qp_eq, Qcmult_assoc. Qed.
-Instance Qp_mult_comm : Comm (=) Qp_mult.
-Proof. intros x y; apply Qp_eq, Qcmult_comm. Qed.
-Lemma Qp_mult_plus_distr_r x y z: (x * (y + z) = x * y + x * z)%Qp.
-Proof. apply Qp_eq, Qcmult_plus_distr_r. Qed.
-Lemma Qp_mult_plus_distr_l x y z: ((x + y) * z = x * z + y * z)%Qp.
-Proof. apply Qp_eq, Qcmult_plus_distr_l. Qed.
-Lemma Qp_mult_1_l x: (1 * x)%Qp = x.
-Proof. apply Qp_eq, Qcmult_1_l. Qed.
-Lemma Qp_mult_1_r x: (x * 1)%Qp = x.
-Proof. apply Qp_eq, Qcmult_1_r. Qed.
+Lemma Qp_1_1 : 1 + 1 = 2.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_add_diag p : p + p = 2 * p.
+Proof. by rewrite <-Qp_1_1, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed.
 
-Lemma Qp_div_1 x : (x / 1 = x)%Qp.
+Lemma Qp_mul_inv_l p : /p * p = 1.
+Proof.
+  destruct p as [p ?]; apply Qp_to_Qc_inj_iff; simpl.
+  by rewrite Qcmult_inv_l, Z2Qc_inj_1 by (by apply not_symmetry, Qclt_not_eq).
+Qed.
+Lemma Qp_mul_inv_r p : p * /p = 1.
+Proof. by rewrite (comm_L Qp_mul), Qp_mul_inv_l. Qed.
+Lemma Qp_inv_mul_distr p q : /(p * q) = /p * /q.
 Proof.
-  apply Qp_eq; simpl.
-  rewrite <-(Qcmult_div_r x 1) at 2 by done. by rewrite Qcmult_1_l.
+  apply (inj (Qp_mul (p * q))).
+  rewrite Qp_mul_inv_r, (comm_L Qp_mul p), <-(assoc_L _), (assoc_L Qp_mul p).
+  by rewrite Qp_mul_inv_r, Qp_mul_1_l, Qp_mul_inv_r.
 Qed.
-Lemma Qp_div_S x y : (x / (2 * y) + x / (2 * y) = x / y)%Qp.
+Lemma Qp_inv_involutive p : / /p = p.
 Proof.
-  apply Qp_eq; simpl. unfold Qcdiv.
-  rewrite <-Qcmult_plus_distr_l, Pos2Z.inj_mul, Z2Qc_inj_mul, Z2Qc_inj_2.
-  rewrite Qcplus_diag. by field_simplify.
+  rewrite <-(Qp_mul_1_l (/ /p)), <-(Qp_mul_inv_r p), <-(assoc_L _).
+  by rewrite Qp_mul_inv_r, Qp_mul_1_r.
 Qed.
-Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp.
+Instance Qp_inv_inj : Inj (=) (=) Qp_inv.
 Proof.
-  change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1.
+  intros p1 p2 Hp. apply (inj (Qp_mul (/p1))).
+  by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l.
 Qed.
-Lemma Qp_half_half : (1 / 2 + 1 / 2 = 1)%Qp.
+Lemma Qp_inv_1 : /1 = 1.
 Proof. apply (bool_decide_unpack _); by compute. Qed.
-Lemma Qp_quarter_three_quarter : (1 / 4 + 3 / 4 = 1)%Qp.
+Lemma Qp_inv_half_half : /2 + /2 = 1.
 Proof. apply (bool_decide_unpack _); by compute. Qed.
-Lemma Qp_three_quarter_quarter : (3 / 4 + 1 / 4 = 1)%Qp.
+Lemma Qp_inv_quarter_quarter : /4 + /4 = /2.
 Proof. apply (bool_decide_unpack _); by compute. Qed.
 
-Lemma Qp_lt_sum (x y : Qp) : (x < y)%Qc ↔ ∃ z, y = (x + z)%Qp.
+Lemma Qp_div_diag p : p / p = 1.
+Proof. apply Qp_mul_inv_r. Qed.
+Lemma Qp_mul_div_l p q : (p / q) * q = p.
+Proof. unfold Qp_div. by rewrite <-(assoc_L _), Qp_mul_inv_l, Qp_mul_1_r. Qed.
+Lemma Qp_mul_div_r p q : q * (p / q) = p.
+Proof. by rewrite (comm_L Qp_mul q), Qp_mul_div_l. Qed.
+Lemma Qp_div_add_distr p q r : (p + q) / r = p / r + q / r.
+Proof. apply Qp_mul_add_distr_r. Qed.
+Lemma Qp_div_div p q r : (p / q) / r = p / (q * r).
+Proof. unfold Qp_div. by rewrite Qp_inv_mul_distr, (assoc_L _). Qed.
+Lemma Qp_div_mul_cancel_l p q r : (r * p) / (r * q) = p / q.
+Proof.
+  rewrite <-Qp_div_div. f_equiv. unfold Qp_div.
+  by rewrite (comm_L Qp_mul r), <-(assoc_L _), Qp_mul_inv_r, Qp_mul_1_r.
+Qed.
+Lemma Qp_div_mul_cancel_r p q r : (p * r) / (q * r) = p / q.
+Proof. by rewrite <-!(comm_L Qp_mul r), Qp_div_mul_cancel_l. Qed.
+Lemma Qp_div_1 p : p / 1 = p.
+Proof. by rewrite <-(Qp_mul_1_r (p / 1)), Qp_mul_div_l. Qed.
+Lemma Qp_div_2 p : p / 2 + p / 2 = p.
+Proof.
+  rewrite <-Qp_div_add_distr, Qp_add_diag.
+  rewrite <-(Qp_mul_1_r 2) at 2. by rewrite Qp_div_mul_cancel_l, Qp_div_1.
+Qed.
+Lemma Qp_div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q.
+Proof. by rewrite <-Qp_div_add_distr, Qp_add_diag, Qp_div_mul_cancel_l. Qed.
+Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p).
+Proof. unfold Qp_div; apply _. Qed.
+Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
+Proof. unfold Qp_div; apply _. Qed.
+
+Instance Qp_le_po : PartialOrder (≤)%Qp.
+Proof.
+  split; [split|].
+  - intros p. by apply Qp_to_Qc_inj_le.
+  - intros p q r. rewrite !Qp_to_Qc_inj_le. by etrans.
+  - intros p q. rewrite !Qp_to_Qc_inj_le, <-Qp_to_Qc_inj_iff. apply Qcle_antisym.
+Qed.
+Instance Qp_lt_strict : StrictOrder (<)%Qp.
 Proof.
   split.
-  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
-    unfold Qcminus. by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
-  - intros [z ->]; simpl.
-    rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf.
+  - intros p ?%Qp_to_Qc_inj_lt. by apply (irreflexivity (<)%Qc (Qp_to_Qc p)).
+  - intros p q r. rewrite !Qp_to_Qc_inj_lt. by etrans.
 Qed.
+Instance Qp_le_total: Total (≤)%Qp.
+Proof. intros p q. rewrite !Qp_to_Qc_inj_le. apply (total Qcle). Qed.
 
-Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp.
+Lemma Qp_lt_le_incl p q : p < q → p ≤ q.
+Proof. rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_weak. Qed.
+Lemma Qp_le_lteq p q : p ≤ q ↔ p < q ∨ p = q.
 Proof.
-  revert q1 q2. cut (∀ q1 q2 : Qp, (q1 ≤ q2)%Qc →
-    ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp).
-  { intros help q1 q2.
-    destruct (Qc_le_dec q1 q2) as [LE|LE%Qclt_nge%Qclt_le_weak]; [by eauto|].
-    destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto. }
-  intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
-  assert (0 < q2 +- q1 */ 2)%Qc as Hq2'.
-  { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq].
-    replace (q1 +- q1 */ 2)%Qc with (q1 * (1 +- 1*/2))%Qc by ring.
-    replace 0%Qc with (0 * (1+-1*/2))%Qc by ring. by apply Qcmult_lt_compat_r. }
-  exists (mk_Qp (q2 +- q1 */ 2%Z) Hq2'). split; [by rewrite Qp_div_2|].
-  apply Qp_eq; simpl. unfold Qcdiv. ring.
+  rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le, <-Qp_to_Qc_inj_iff. split.
+  - intros [?| ->]%Qcle_lt_or_eq; auto.
+  - intros [?| ->]; auto using Qclt_le_weak.
 Qed.
+Lemma Qp_lt_ge_cases p q : {p < q} + {q ≤ p}.
+Proof.
+  refine (cast_if (Qclt_le_dec (Qp_to_Qc p) (Qp_to_Qc q)%Qc));
+    [by apply Qp_to_Qc_inj_lt|by apply Qp_to_Qc_inj_le].
+Defined.
+Lemma Qp_le_lt_trans p q r : p ≤ q → q < r → p < r.
+Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcle_lt_trans. Qed.
+Lemma Qp_lt_le_trans p q r : p < q → q ≤ r → p < r.
+Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_trans. Qed.
 
-Lemma Qp_lower_bound_lt (q1 q2 : Qp) : ∃ q : Qp, q < q1 ∧ q < q2.
+Lemma Qp_le_ngt p q : p ≤ q ↔ ¬q < p.
 Proof.
-  destruct (Qp_lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]).
-  exists qmin. split; eapply Qp_lt_sum; eauto.
+  rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le.
+  split; auto using Qcle_not_lt, Qcnot_lt_le.
+Qed.
+Lemma Qp_lt_nge p q : p < q ↔ ¬q ≤ p.
+Proof.
+  rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le.
+  split; auto using Qclt_not_le, Qcnot_le_lt.
 Qed.
 
-Lemma Qp_cross_split p a b c d :
-  (a + b = p → c + d = p →
-  ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
+Lemma Qp_add_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q.
+Proof. rewrite !Qp_to_Qc_inj_le. destruct p, q, r; apply Qcplus_le_mono_l. Qed.
+Lemma Qp_add_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r.
+Proof. rewrite !(comm_L Qp_add _ r). apply Qp_add_le_mono_l. Qed.
+Lemma Qp_add_le_mono q p n m : q ≤ n → p ≤ m → q + p ≤ n + m.
+Proof. intros. etrans; [by apply Qp_add_le_mono_l|by apply Qp_add_le_mono_r]. Qed.
+
+Lemma Qp_add_lt_mono_l p q r : p < q ↔ r + p < r + q.
+Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_l. Qed.
+Lemma Qp_add_lt_mono_r p q r : p < q ↔ p + r < q + r.
+Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_r. Qed.
+Lemma Qp_add_lt_mono q p n m : q < n → p < m → q + p < n + m.
+Proof. intros. etrans; [by apply Qp_add_lt_mono_l|by apply Qp_add_lt_mono_r]. Qed.
+
+Lemma Qp_mul_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q.
 Proof.
-  intros H <-. revert a b c d H. cut (∀ a b c d : Qp,
-    (a < c)%Qc → a + b = c + d →
-    ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
-  { intros help a b c d Habcd.
-    destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq].
-    - auto.
-    - destruct (help c d a b); [done..|]. naive_solver.
-    - apply (inj (Qp_plus a)) in Habcd as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
-      exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_plus). }
-  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)).
-  destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
-  eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L Qp_plus)|..|done].
-  - by rewrite (assoc_L _), (comm_L Qp_plus e).
-  - by rewrite (assoc_L _), (comm_L Qp_plus a').
+  rewrite !Qp_to_Qc_inj_le. destruct p, q, r; by apply Qcmult_le_mono_pos_l.
 Qed.
+Lemma Qp_mul_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r.
+Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_le_mono_l. Qed.
+Lemma Qp_mul_le_mono q p n m : q ≤ n → p ≤ m → q * p ≤ n * m.
+Proof. intros. etrans; [by apply Qp_mul_le_mono_l|by apply Qp_mul_le_mono_r]. Qed.
 
-Lemma Qp_bounded_split (p r : Qp) : ∃ q1 q2 : Qp, (q1 ≤ r)%Qc ∧ p = (q1 + q2)%Qp.
+Lemma Qp_mul_lt_mono_l p q r : p < q ↔ r * p < r * q.
 Proof.
-  destruct (Qclt_le_dec r p) as [?|?].
-  - assert (0 < p +- r)%Qc as Hpos.
-    { apply (Qcplus_lt_mono_r _ _ r). rewrite <-Qcplus_assoc, (Qcplus_comm (-r)).
-      by rewrite Qcplus_opp_r, Qcplus_0_l, Qcplus_0_r. }
-    exists r, (mk_Qp _ Hpos); simpl; split; [done|].
-    apply Qp_eq; simpl. rewrite Qcplus_comm, <-Qcplus_assoc, (Qcplus_comm (-r)).
-    by rewrite Qcplus_opp_r, Qcplus_0_r.
-  - exists (p / 2)%Qp, (p / 2)%Qp; split.
-    + trans p; [|done]. apply Qclt_le_weak, Qp_lt_sum.
-      exists (p / 2)%Qp. by rewrite Qp_div_2.
-    + by rewrite Qp_div_2.
+  rewrite !Qp_to_Qc_inj_lt. destruct p, q, r; by apply Qcmult_lt_mono_pos_l.
 Qed.
+Lemma Qp_mul_lt_mono_r p q r : p < q ↔ p * r < q * r.
+Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_lt_mono_l. Qed.
+Lemma Qp_mul_lt_mono q p n m : q < n → p < m → q * p < n * m.
+Proof. intros. etrans; [by apply Qp_mul_lt_mono_l|by apply Qp_mul_lt_mono_r]. Qed.
 
-Lemma Qp_not_plus_ge (q p : Qp) : ¬ (q + p)%Qp ≤ q.
+Lemma Qp_lt_add_l p q : p < p + q.
 Proof.
-  rewrite <- (Qcplus_0_r q).
-  intros Hle%(Qcplus_le_mono_l p 0 q)%Qcle_ngt.
-  apply Hle, Qp_prf.
+  destruct p as [p ?], q as [q ?]. apply Qp_to_Qc_inj_lt; simpl.
+  rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l.
 Qed.
+Lemma Qp_lt_add_r p q : q < p + q.
+Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_l. Qed.
+
+Lemma Qp_not_add_le_l p q : ¬(p + q ≤ p).
+Proof. apply Qp_lt_nge, Qp_lt_add_l. Qed.
+Lemma Qp_not_add_le_r p q : ¬(p + q ≤ q).
+Proof. apply Qp_lt_nge, Qp_lt_add_r. Qed.
+
+Lemma Qp_add_id_free q p : q + p ≠ q.
+Proof. intro Heq. apply (Qp_not_add_le_l q p). by rewrite Heq. Qed.
 
-Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
-Proof. apply Qclt_le_weak, Qp_prf. Qed.
+Lemma Qp_le_add_l p q : p ≤ p + q.
+Proof. apply Qp_lt_le_incl, Qp_lt_add_l. Qed.
+Lemma Qp_le_add_r p q : q ≤ p + q.
+Proof. apply Qp_lt_le_incl, Qp_lt_add_r. Qed.
 
-Lemma Qp_le_plus_r (q p : Qp) : p ≤ q + p.
+Lemma Qp_sub_Some p q r : p - q = Some r ↔ p = q + r.
 Proof.
-  apply (Qcplus_le_mono_l _ _ (-p)%Qc). rewrite Qcplus_comm, Qcplus_opp_r.
-  rewrite Qcplus_comm, <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r. apply Qp_ge_0.
+  destruct p as [p Hp], q as [q Hq], r as [r Hr].
+  unfold Qp_sub, Qp_add; simpl; rewrite <-Qp_to_Qc_inj_iff; simpl. split.
+  - intros; simplify_option_eq. unfold Qcminus.
+    by rewrite (Qcplus_comm p), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
+  - intros ->. unfold Qcminus.
+    rewrite <-Qcplus_assoc, (Qcplus_comm r), Qcplus_assoc.
+    rewrite Qcplus_opp_r, Qcplus_0_l. simplify_option_eq; [|done].
+    f_equal. by apply Qp_to_Qc_inj_iff.
+Qed.
+Lemma Qp_lt_sum p q : p < q ↔ ∃ r, q = p + r.
+Proof.
+  destruct p as [p Hp], q as [q Hq]. rewrite Qp_to_Qc_inj_lt; simpl.
+  split.
+  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt).
+    apply Qp_to_Qc_inj_iff; simpl. unfold Qcminus.
+    by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
+  - intros [[r ?] ?%Qp_to_Qc_inj_iff]; simplify_eq/=.
+    rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l.
 Qed.
 
-Lemma Qp_le_plus_l (q p : Qp) : q ≤ q + p.
-Proof. rewrite Qcplus_comm. apply Qp_le_plus_r. Qed.
+Lemma Qp_sub_None p q : p - q = None ↔ p ≤ q.
+Proof.
+  rewrite Qp_le_ngt, Qp_lt_sum, eq_None_not_Some.
+  by setoid_rewrite <-Qp_sub_Some.
+Qed.
+Lemma Qp_sub_diag p : p - p = None.
+Proof. by apply Qp_sub_None. Qed.
+Lemma Qp_add_sub p q : (p + q) - q = Some p.
+Proof. apply Qp_sub_Some. by rewrite (comm_L Qp_add). Qed.
 
-Lemma Qp_le_plus_compat (q p n m : Qp) : q ≤ n → p ≤ m → q + p ≤ n + m.
+Lemma Qp_inv_lt_mono p q : p < q ↔ /q < /p.
 Proof.
-  intros. eapply Qcle_trans; [by apply Qcplus_le_mono_l
-                             |by apply Qcplus_le_mono_r].
+  revert p q. cut (∀ p q, p < q → / q < / p).
+  { intros help p q. split; [apply help|]. intros.
+    rewrite <-(Qp_inv_involutive p), <-(Qp_inv_involutive q). by apply help. }
+  intros p q Hpq. apply (Qp_mul_lt_mono_l _ _ q). rewrite Qp_mul_inv_r.
+  apply (Qp_mul_lt_mono_r _ _ p). rewrite <-(assoc_L _), Qp_mul_inv_l.
+  by rewrite Qp_mul_1_l, Qp_mul_1_r.
 Qed.
+Lemma Qp_inv_le_mono p q : p ≤ q ↔ /q ≤ /p.
+Proof. by rewrite !Qp_le_ngt, Qp_inv_lt_mono. Qed.
 
-Lemma Qp_plus_id_free q p : q + p = q → False.
-Proof. intro Heq. apply (Qp_not_plus_ge q p). by rewrite Heq.  Qed.
+Lemma Qp_div_le_mono_l p q r : q ≤ p ↔ r / p ≤ r / q.
+Proof. unfold Qp_div. by rewrite <-Qp_mul_le_mono_l, Qp_inv_le_mono. Qed.
+Lemma Qp_div_le_mono_r p q r : p ≤ q ↔ p / r ≤ q / r.
+Proof. apply Qp_mul_le_mono_r. Qed.
+Lemma Qp_div_lt_mono_l p q r : q < p ↔ r / p < r / q.
+Proof. unfold Qp_div. by rewrite <-Qp_mul_lt_mono_l, Qp_inv_lt_mono. Qed.
+Lemma Qp_div_lt_mono_r p q r : p < q ↔ p / r < q / r.
+Proof. apply Qp_mul_lt_mono_r. Qed.
 
-Lemma Qp_plus_weak_r (q p o : Qp) : q + p ≤ o → q ≤ o.
-Proof. intros Le. eapply Qcle_trans; [ apply Qp_le_plus_l | apply Le ]. Qed.
+Lemma Qp_div_lt p q : 1 < q → p / q < p.
+Proof. by rewrite (Qp_div_lt_mono_l _ _ p), Qp_div_1. Qed.
+Lemma Qp_div_le p q : 1 ≤ q → p / q ≤ p.
+Proof. by rewrite (Qp_div_le_mono_l _ _ p), Qp_div_1. Qed.
 
-Lemma Qp_plus_weak_l (q p o : Qp) : q + p ≤ o → p ≤ o.
-Proof. rewrite Qcplus_comm. apply Qp_plus_weak_r. Qed.
+Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'.
+Proof.
+  revert q1 q2. cut (∀ q1 q2 : Qp, q1 ≤ q2 →
+    ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2').
+  { intros help q1 q2.
+    destruct (Qp_lt_ge_cases q2 q1) as [Hlt|Hle]; eauto.
+    destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto using Qp_lt_le_incl. }
+  intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
+  assert (q1 / 2 < q2) as [q2' ->]%Qp_lt_sum.
+  { eapply Qp_lt_le_trans, Hq. by apply Qp_div_lt. }
+  eexists; split; [|done]. by rewrite Qp_div_2.
+Qed.
+
+Lemma Qp_lower_bound_lt q1 q2 : ∃ q : Qp, q < q1 ∧ q < q2.
+Proof.
+  destruct (Qp_lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]).
+  exists qmin. split; eapply Qp_lt_sum; eauto.
+Qed.
 
-Lemma Qp_plus_weak_2_r (q p o : Qp) : q ≤ o → q ≤ p + o.
-Proof. intros Le. eapply Qcle_trans; [apply Le| apply Qp_le_plus_r]. Qed.
+Lemma Qp_cross_split p a b c d :
+  a + b = p → c + d = p →
+  ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d.
+Proof.
+  intros H <-. revert a b c d H. cut (∀ a b c d : Qp,
+    a < c → a + b = c + d →
+    ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
+  { intros help a b c d Habcd.
+    destruct (Qp_lt_ge_cases a c) as [?|[?| ->]%Qp_le_lteq].
+    - auto.
+    - destruct (help c d a b); [done..|]. naive_solver.
+    - apply (inj (Qp_add a)) in Habcd as ->.
+      destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
+      exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_add). }
+  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_add a)).
+  destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
+  eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L Qp_add)|..|done].
+  - by rewrite (assoc_L _), (comm_L Qp_add e).
+  - by rewrite (assoc_L _), (comm_L Qp_add a').
+Qed.
 
-Lemma Qp_plus_weak_2_l (q p o : Qp) : q ≤ p → q ≤ p + o.
-Proof. rewrite Qcplus_comm. apply Qp_plus_weak_2_r. Qed.
+Lemma Qp_bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2.
+Proof.
+  destruct (Qp_lt_ge_cases r p) as [[q ->]%Qp_lt_sum|?].
+  { by exists r, q. }
+  exists (p / 2)%Qp, (p / 2)%Qp; split.
+  + trans p; [|done]. by apply Qp_div_le.
+  + by rewrite Qp_div_2.
+Qed.
 
-Lemma Qp_max_spec (q p : Qp) : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
+Lemma Qp_max_spec q p : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
 Proof.
   unfold Qp_max.
-  destruct (decide (q ≤ p)) as [[?| ->%Qp_eq]%Qcle_lt_or_eq|?]; [by auto..|].
-  right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt.
+  destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lteq|?]; [by auto..|].
+  right. split; [|done]. by apply Qp_lt_le_incl, Qp_lt_nge.
 Qed.
 
-Lemma Qp_max_spec_le (q p : Qp) : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
-Proof. destruct (Qp_max_spec q p) as [[?%Qclt_le_weak?]|]; [left|right]; done. Qed.
+Lemma Qp_max_spec_le q p : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
+Proof. destruct (Qp_max_spec q p) as [[?%Qp_lt_le_incl?]|]; [left|right]; done. Qed.
 
 Instance Qp_max_assoc : Assoc (=) Qp_max.
 Proof.
   intros q p o. unfold Qp_max. destruct (decide (q ≤ p)), (decide (p ≤ o));
-    eauto using decide_True, Qcle_trans.
+    try by rewrite ?decide_True by (by etrans).
   rewrite decide_False by done.
-  by rewrite decide_False by (eapply Qclt_not_le, Qclt_trans; by apply Qclt_nge).
+  by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge).
 Qed.
 Instance Qp_max_comm : Comm (=) Qp_max.
 Proof.
-  intros q p. apply Qp_eq.
-  destruct (Qp_max_spec_le q p) as [[?->]|[?->]], (Qp_max_spec_le p q) as [[?->]|[?->]];
-    eauto using Qcle_antisym.
+  intros q p.
+  destruct (Qp_max_spec_le q p) as [[?->]|[?->]],
+    (Qp_max_spec_le p q) as [[?->]|[?->]]; done || by apply (anti_symm (≤)).
 Qed.
 
 Lemma Qp_max_id q : q `max` q = q.
 Proof. by destruct (Qp_max_spec q q) as [[_->]|[_->]]. Qed.
 
-Lemma Qp_le_max_l (q p : Qp) : q ≤ q `max` p.
+Lemma Qp_le_max_l q p : q ≤ q `max` p.
 Proof. unfold Qp_max. by destruct (decide (q ≤ p)). Qed.
+Lemma Qp_le_max_r q p : p ≤ q `max` p.
+Proof. rewrite (comm_L Qp_max q). apply Qp_le_max_l. Qed.
 
-Lemma Qp_le_max_r (q p : Qp) : p ≤ q `max` p.
-Proof. rewrite (comm _ q). apply Qp_le_max_l. Qed.
-
-Lemma Qp_max_plus (q p : Qp) : q `max` p ≤ q + p.
-Proof.
-  unfold Qp_max. destruct (decide (q ≤ p)).
-  - apply Qp_le_plus_r.
-  - apply Qp_le_plus_l.
-Qed.
-
-Lemma Qp_max_lub_l (q p o : Qp) : q `max` p ≤ o → q ≤ o.
+Lemma Qp_max_add q p : q `max` p ≤ q + p.
 Proof.
-  unfold Qp_max. destruct (decide (q ≤ p)); [by apply Qcle_trans | done].
+  unfold Qp_max.
+  destruct (decide (q ≤ p)); [apply Qp_le_add_r|apply Qp_le_add_l].
 Qed.
 
-Lemma Qp_max_lub_r (q p o : Qp) : q `max` p ≤ o → p ≤ o.
+Lemma Qp_max_lub_l q p o : q `max` p ≤ o → q ≤ o.
+Proof. unfold Qp_max. destruct (decide (q ≤ p)); [by etrans|done]. Qed.
+Lemma Qp_max_lub_r q p o : q `max` p ≤ o → p ≤ o.
 Proof. rewrite (comm _ q). apply Qp_max_lub_l. Qed.
 
-Lemma Qp_min_spec (q p : Qp) : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
+Lemma Qp_min_spec q p : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
 Proof.
   unfold Qp_min.
-  destruct (decide (q ≤ p)) as [[?| ->%Qp_eq]%Qcle_lt_or_eq|?]; [by auto..|].
-  right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt.
+  destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lteq|?]; [by auto..|].
+  right. split; [|done]. by apply Qp_lt_le_incl, Qp_lt_nge.
 Qed.
 
-Lemma Qp_min_spec_le (q p : Qp) : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
-Proof. destruct (Qp_min_spec q p) as [[?%Qclt_le_weak?]|]; [left|right]; done. Qed.
+Lemma Qp_min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
+Proof. destruct (Qp_min_spec q p) as [[?%Qp_lt_le_incl ?]|]; [left|right]; done. Qed.
 
 Instance Qp_min_assoc : Assoc (=) Qp_min.
 Proof.
   intros q p o. unfold Qp_min.
   destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False.
-  - rewrite decide_True by done. by rewrite decide_True by (eapply Qcle_trans; done).
-  - by rewrite (decide_False _ _) by (eapply Qclt_not_le, Qclt_trans; by apply Qclt_nge).
+  - by rewrite !decide_True by (by etrans).
+  - by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge).
 Qed.
 Instance Qp_min_comm : Comm (=) Qp_min.
 Proof.
-  intros q p. apply Qp_eq.
-  destruct (Qp_min_spec_le q p) as [[?->]|[?->]], (Qp_min_spec_le p q) as [[? ->]|[? ->]];
-    eauto using Qcle_antisym.
+  intros q p.
+  destruct (Qp_min_spec_le q p) as [[?->]|[?->]],
+    (Qp_min_spec_le p q) as [[? ->]|[? ->]]; done || by apply (anti_symm (≤)).
 Qed.
 
-Lemma Qp_min_id (q : Qp) : q `min` q = q.
+Lemma Qp_min_id q : q `min` q = q.
 Proof. by destruct (Qp_min_spec q q) as [[_->]|[_->]]. Qed.
-
-Lemma Qp_le_min_r (q p : Qp) : q `min` p ≤ p.
+Lemma Qp_le_min_r q p : q `min` p ≤ p.
 Proof. by destruct (Qp_min_spec_le q p) as [[?->]|[?->]]. Qed.
 
-Lemma Qp_le_min_l (p q : Qp) : p `min` q ≤ p.
-Proof. rewrite (comm _ p). apply Qp_le_min_r. Qed.
+Lemma Qp_le_min_l p q : p `min` q ≤ p.
+Proof. rewrite (comm_L Qp_min p). apply Qp_le_min_r. Qed.
 
-Lemma Qp_min_l_iff (q p : Qp) : q `min` p = q ↔ q ≤ p.
+Lemma Qp_min_l_iff q p : q `min` p = q ↔ q ≤ p.
 Proof.
   destruct (Qp_min_spec_le q p) as [[?->]|[?->]]; [done|].
-  split; [by intros ->|]. intros. by apply Qp_eq, Qcle_antisym.
+  split; [by intros ->|]. intros. by apply (anti_symm (≤)).
 Qed.
+Lemma Qp_min_r_iff q p : q `min` p = p ↔ p ≤ q.
+Proof. rewrite (comm_L Qp_min q). apply Qp_min_l_iff. Qed.
 
-Lemma Qp_min_r_iff (q p : Qp) : q `min` p = p ↔ p ≤ q.
-Proof. rewrite (comm _ q). apply Qp_min_l_iff. Qed.
+Lemma pos_to_Qp_1 : pos_to_Qp 1 = 1.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma pos_to_Qp_inj n m : pos_to_Qp n = pos_to_Qp m → n = m.
+Proof. by injection 1. Qed.
+Lemma pos_to_Qp_inj_iff n m : pos_to_Qp n = pos_to_Qp m ↔ n = m.
+Proof. split; [apply pos_to_Qp_inj|by intros ->]. Qed.
+Lemma pos_to_Qp_inj_le n m : (n ≤ m)%positive ↔ pos_to_Qp n ≤ pos_to_Qp m.
+Proof. rewrite Qp_to_Qc_inj_le; simpl. by rewrite <-Z2Qc_inj_le. Qed.
+Lemma pos_to_Qp_inj_lt n m : (n < m)%positive ↔ pos_to_Qp n < pos_to_Qp m.
+Proof. by rewrite Pos.lt_nle, Qp_lt_nge, <-pos_to_Qp_inj_le. Qed.
+Lemma pos_to_Qp_add x y : pos_to_Qp x + pos_to_Qp y = pos_to_Qp (x + y).
+Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_add, Z2Qc_inj_add. Qed.
+Lemma pos_to_Qp_mul x y : pos_to_Qp x * pos_to_Qp y = pos_to_Qp (x * y).
+Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. Qed.
 
 Local Close Scope Qp_scope.
-Local Close Scope Qc_scope.
 
 (** * Helper for working with accessing lists with wrap-around
     See also [rotate] and [rotate_take] in [list.v] *)