diff --git a/opam b/opam
index e41b3f1e48e3899425c4e9b647fd9f4fded83a2e..094bd18e5cec2f5fdef378f80c78ec7482782d5c 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-10-21.0.e29403ca") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-10-30.0.93f5a686") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index bfc7200d07911f36960d4da42d34e4f521fc1e5d..a085a0179fd13466f8af703fb0114cb8e64f388b 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl csum frac auth agree.
@@ -270,10 +269,6 @@ End ArcInv.
 
 Typeclasses Opaque StrongTok WeakTok StrMoves StrDowns WkUps.
 
-Lemma Qp_plus_div (x y : Qp) n:
-  (x/n + y/n)%Qp = ((x+y) / n)%Qp.
-Proof. apply Qp_eq; simpl. by rewrite -Qcmult_plus_distr_l. Qed.
-
 Section arc.
   (* P1 is the thing that is shared by strong reference owners (in practice,
      this is the lifetime token), and P2 is the thing that is owned by the
@@ -614,7 +609,7 @@ Section arc.
     iDestruct "Own" as (γsw)
       "(SA & St & WA & SMA & [SM1 SM2] & SDA & [SD1 SD2] & WUA & WU & [S1 S2])".
     iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
-      first by rewrite -Qp_plus_assoc 2!Qp_div_2.
+      first by rewrite -Qp_add_assoc 2!Qp_div_2.
     set Qs : time → time → gname → gname → vProp :=
       (λ ts tw γs γw,
         GPS_SWSharedReader l ts (() : unitProtocol) #1 (1/2)%Qp γs ∗
@@ -670,7 +665,7 @@ Section arc.
         [|rewrite left_id]; by apply auth_auth_valid. }
     iDestruct "Own" as (γsw) "(SA & WA & Wt & SMA & SM & SDA & SD & WUA & [WU1 WU2])".
     iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
-      first by rewrite -Qp_plus_assoc 2!Qp_div_2.
+      first by rewrite -Qp_add_assoc 2!Qp_div_2.
     set Qs : time → time → gname → gname → vProp :=
       (λ ts tw γs γw,
         GPS_SWSharedReader (l >> 1) tw (() : unitProtocol) #1 (1 / 2)%Qp γw ∗
@@ -959,7 +954,7 @@ Section arc.
         iExists _. by iFrame "St' tok2 R2 SM2 HP2 MAX SD2 OS2".
       - iExists (Some ((q' + q'' / 2)%Qp, (n + 1)%positive)). iSplitL ""; [done|].
         iFrame "SA W'". iExists (q''/2)%Qp.
-        iSplitL "". { iPureIntro. by rewrite -Qp_plus_assoc Qp_div_2. }
+        iSplitL "". { iPureIntro. by rewrite -Qp_add_assoc Qp_div_2. }
         iFrame "HP1". iExists Mt', Dt'. iFrame "tok1 R1 SM1 SeenM' SD1 SeenD OS1". }
 
     (* finally done with the CAS *)
@@ -1148,7 +1143,7 @@ Section arc.
         + iExists (Some 1%Qp, Some $ Cinl ((q' + q'' / 2)%Qp, (n + 1)%positive)).
           iSplitL ""; [done|]. iFrame "WA W'". iSplit; [done|].
           iExists (q''/2)%Qp, Ut'. iFrame "tok1 R1 WU1 SeenU".
-          iPureIntro. by rewrite -Qp_plus_assoc Qp_div_2.
+          iPureIntro. by rewrite -Qp_add_assoc Qp_div_2.
       - iDestruct "WI" as "(>Eq & $ & WI)". iDestruct "Eq" as %?. subst qs.
         iDestruct "WI" as (Ut') "([tok1 tok2] & R & WU & #SeenU)".
         iModIntro. iExists (). iSplitL""; [done|]. iIntros (t'' Lt'') "W'".
@@ -1313,7 +1308,7 @@ Section arc.
           iFrame "Wt SDA". iExists _. iFrame "St' tok2 R2 WU2".
         + iExists (Some iS, Some $ Cinl ((q' + q'' / 2)%Qp, (n + 1)%positive)).
           iSplitL ""; [done|]. iFrame (iSI) "WA W'". iExists (q''/2)%Qp, Ut'.
-          iFrame "tok1 R1 WU1 SeenU". iPureIntro. by rewrite -Qp_plus_assoc Qp_div_2.
+          iFrame "tok1 R1 WU1 SeenU". iPureIntro. by rewrite -Qp_add_assoc Qp_div_2.
       - iDestruct "WI" as "($ & WI & HP2 & tokM & SW & SM & SD)".
         iDestruct "WI" as (q'' Ut') "(>Eq'' & tok & R & WU & #SeenU)".
         iDestruct "Eq''" as %Eq''. rewrite /StrDowns. iDestruct "SD" as (Dt') ">SD".
@@ -1350,7 +1345,7 @@ Section arc.
           iSplitL ""; [done|]. iFrame "WA W' HP2 tokM SW SM".
           iSplitR "SD"; [|by iExists _].
           iExists (q''/2)%Qp, Ut'. iFrame "tok1 R1 WU1 SeenU".
-          iPureIntro. by rewrite -Qp_plus_assoc Qp_div_2. }
+          iPureIntro. by rewrite -Qp_add_assoc Qp_div_2. }
 
     (* finally done with the CAS *)
     iIntros "!>" (b t' [] v') "(IW &%& [([%[%%]]&R'&Q) | ([%[_ %]] &R'&Rs&_)])".
@@ -1507,7 +1502,7 @@ Section arc.
         iDestruct "MAX4" as %MAX. iPureIntro. move => ? /MAX ->. by rewrite Ext4.
       - iExists (Some ((q' + q'' / 2)%Qp, (n + 1)%positive)).
         iSplitL ""; [done|]. iFrame "SA W'". iExists (q''/2)%Qp.
-        iSplitL ""; [by rewrite -Qp_plus_assoc Qp_div_2|].
+        iSplitL ""; [by rewrite -Qp_add_assoc Qp_div_2|].
         iFrame "HP1". iExists Mt', Dt'. iFrame "tok1 SR1 SM1 SD1 SeenD oW1".
         iExists _,_. by iFrame "SR4 MAX4". }
 
@@ -1648,7 +1643,7 @@ Section arc.
           - subst n. simpl in Eq'. subst q'.
             by iApply (WeakAuth_drop_last with "[$WA $Wt]").
           - rewrite (decide_False _ _ NEq) in Eq'. destruct Eq' as [q3 Eq3].
-            iExists q3. iFrame (Eq3). rewrite Eq3 Qp_plus_comm.
+            iExists q3. iFrame (Eq3). rewrite Eq3 Qp_add_comm.
             rewrite {1}(_: n = (1 + Pos.pred n)%positive);
               first by iApply (WeakAuth_drop with "[$WA $Wt]").
             by rewrite -Pplus_one_succ_l Pos.succ_pred. }
@@ -1661,7 +1656,7 @@ Section arc.
         iCombine "SeenU" "SeenU'" as "SeenU'".
         iDestruct (SeenActs_join with "SeenU'") as "SeenU'".
         rewrite decide_False; last lia.
-        iCombine "tok" "tok'" as "tok". rewrite Qp_plus_div.
+        iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr.
         case (decide (n = 1%positive)) => nEq.
         + subst n. simpl in Eq'. subst q'. iExists (Some 1%Qp, None).
           iSplitL""; [done|]. iFrame "WA W'". iSplitL ""; [done|]. iExists _.
@@ -1672,7 +1667,7 @@ Section arc.
             by rewrite Z.add_1_r -Pos2Z.inj_succ Pos.succ_pred. }
           iFrame "WA W'". iSplitL ""; [done|]. iExists (q + q'')%Qp,_.
           iFrame "tok R WU SeenU'".
-          iPureIntro. by rewrite Qp_plus_assoc (Qp_plus_comm q2).
+          iPureIntro. by rewrite Qp_add_assoc (Qp_add_comm q2).
       - iDestruct "WI" as "($ & WI & HP & tokS & SW & SM & SD)".
         iDestruct "WI" as (q'' Ut') "(Eq'' & tok' & R & WU' & SeenU')".
         iDestruct "Eq''" as %Eq''. rewrite /StrDowns.
@@ -1704,7 +1699,7 @@ Section arc.
           - subst n. simpl in Eq'. subst q'.
             by iApply (WeakAuth_drop_last with "[$WA $Wt]").
           - rewrite (decide_False _ _ NEq) in Eq'. destruct Eq' as [q3 Eq3].
-            iExists q3. iFrame (Eq3). rewrite Eq3 Qp_plus_comm.
+            iExists q3. iFrame (Eq3). rewrite Eq3 Qp_add_comm.
             rewrite {1}(_: n = (1 + Pos.pred n)%positive);
               first by iApply (WeakAuth_drop with "[$WA $Wt]").
             by rewrite -Pplus_one_succ_l Pos.succ_pred. }
@@ -1730,8 +1725,8 @@ Section arc.
           { iPureIntro. f_equal. by rewrite Z.sub_1_r -Pos2Z.inj_pred. }
           iFrame "WA W' HP tokS SW SM". subst q'. iSplitR "SD"; [|by iExists _].
           iExists (q + q'')%Qp, _.
-          iCombine "tok" "tok'" as "tok". rewrite Qp_plus_div.
-          iFrame "R' tok WU SeenU'". by rewrite Qp_plus_assoc (Qp_plus_comm q2). }
+          iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr.
+          iFrame "R' tok WU SeenU'". by rewrite assoc_L (comm_L _ q2). }
 
     (* finally done with the CAS *)
     iIntros "!>" (b t2 [] v2) "(_ & [((%&%&%)&QI) | ((%&_&%)&IW&R'&_&P&IS)])";
@@ -1793,7 +1788,7 @@ Section arc.
     iIntros "!> (WW & WR & tok' & WU & P2 & tokh & SW & SM & SD)".
     iDestruct "WU" as (Uw) "[WU _]". iDestruct "SM" as (Ms) "SM".
     iDestruct "tok'" as (q'' Eq'') "tok'".
-    iCombine "tok" "tok'" as "tok". rewrite Qp_plus_div Eq''.
+    iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq''.
     iCombine "tokh" "tok" as "tok".
 
     iApply wp_fupd. iApply wp_hist_inv; [done|]. iIntros "#HINV". wp_let.
@@ -2144,7 +2139,7 @@ Section arc.
         - subst n. simpl in Eq'. subst q'.
           by iApply (StrongAuth_drop_last with "[$SA $St]").
         - rewrite (decide_False _ _ NEq) in Eq'. destruct Eq' as [q3 Eq3].
-          iExists q3. iFrame (Eq3). rewrite Eq3 Qp_plus_comm.
+          iExists q3. iFrame (Eq3). rewrite Eq3 Qp_add_comm.
           rewrite {1}(_: n = (1 + Pos.pred n)%positive);
             first by iApply (StrongAuth_drop with "[$SA $St]").
           by rewrite -Pplus_one_succ_l Pos.succ_pred. }
@@ -2172,11 +2167,11 @@ Section arc.
         iExists (Some (q2, Pos.pred n)). iSplitL "".
         { iPureIntro. f_equal. by rewrite Z.sub_1_r -Pos2Z.inj_pred. }
         iFrame "SA W'". subst q'. iExists (q + q'')%Qp. iSplitL "".
-        { by rewrite Qp_plus_assoc (Qp_plus_comm q2). } iFrame "HP".
+        { by rewrite Qp_add_assoc (Qp_add_comm q2). } iFrame "HP".
         iExists _,_. iFrame "R' SM SD SeenD' oW".
         rewrite /Mt' (decide_False _ _ nEq). iFrame "SeenM'".
         rewrite decide_False; last first. { simpl. by destruct n; try lia. }
-        rewrite -Qp_plus_div. by iFrame "tok tok'". }
+        rewrite Qp_div_add_distr. by iFrame "tok tok'". }
 
     (* finally done with the CAS *)
     iIntros "!>" (b t2 [] v2) "(_ & [((%&%&%)&QI) | ((%&_&%)&IS&R'&_&P&IW)])";
@@ -2252,7 +2247,7 @@ Section arc.
     iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
     { by iApply (arc_inv_join with "SMA SDA WUA IS IW"). }
 
-    iCombine "tok" "tok'" as "tok". rewrite Qp_plus_div Eq''.
+    iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq''.
     iModIntro. iApply "HΦ". iFrame "HP tok". iSplitL "SW"; [by iExists _|].
     iSplitL "SM SeenM'"; [iExists _; by iFrame|].
     iSplitL "SD SeenD'"; [iExists _; by iFrame|]. by iFrame "oW".
@@ -2367,7 +2362,7 @@ Section arc.
     iIntros "!> (SW & HP & tok' & SR & SM & SD & oW)".
     iDestruct "SM" as (Mt2) "[SM SeenM']". iDestruct "SD" as (Dt2) "[SD SeenD']".
     iDestruct "tok'" as (q'' Eq'') "tok'".
-    iCombine "tok" "tok'" as "tok". rewrite Qp_plus_div Eq''.
+    iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq''.
 
     iApply wp_fupd. wp_let.
     (* open invariant to revert shared writer to strong writer *)
@@ -2518,7 +2513,7 @@ Section arc.
         iDestruct (GPS_SWSharedReaders_join with "SR' SR") as "SR'".
         iDestruct (StrMoves_agree with "[$SM $SM']") as %?. subst Mt2.
         iCombine "SM" "SM'" as "SM". iCombine "HP1" "HP2" as "HP".
-        iCombine "tok" "tok'" as "tok". rewrite HPn Qp_plus_comm Qp_plus_div Eq''.
+        iCombine "tok" "tok'" as "tok". rewrite HPn Qp_add_comm -Qp_div_add_distr Eq''.
         iCombine "tok" "tokW" as "tok". iDestruct ("FR" with "tok VR") as "#$".
         by iFrame "SR' SMA WUA SM HP tok VR".
       - (* it's impossible to read 1 with only F_read *)
@@ -2754,7 +2749,7 @@ Section arc.
         iDestruct (WeakAuth_strong with "[$WA $oW]") as %[qs ?]. subst iS.
         destruct st as [[[]| |]|]. exfalso. lia. by exfalso. by exfalso.
         iDestruct "WI" as "(% & $ & WI)". iDestruct "WI" as (Ut) "(tokW&?&WU&?)".
-        iCombine "tok" "tok'" as "tok". rewrite Qp_plus_div Eq.
+        iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq.
         iCombine "tok" "tokW" as "tok". iDestruct ("FR" with "tok VR") as "#$".
         iModIntro. by iFrame "tok VR".
       - iDestruct 1 as (st Eq') "[_ WI]". inversion Eq' as [Eq1]. clear Eq'.
@@ -2778,7 +2773,7 @@ Section arc.
       iDestruct "Rs" as "[Rs oW]". iDestruct "Rs" as (z) "%". subst v2.
       iModIntro. wp_op. rewrite bool_decide_false; [|move => ?; exfalso; by subst z].
       wp_case. iApply ("HΦ" $! 1%fin). simpl. iFrame "HP1".
-      iCombine "tok" "tok'" as "tok". rewrite Qp_plus_div Eq. iFrame "tok".
+      iCombine "tok" "tok'" as "tok". rewrite -Qp_div_add_distr Eq. iFrame "tok".
       iSplitL "SW"; [by iExists _|]. iSplitL "SM". { iExists _. iFrame "SM SeenM". }
       iFrame "oW". iExists _. iFrame "SD". iExists _, _. iFrame (MAX) "WR". }
 
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 81a09112264ad992821c6a1e99d6ac6aaff1d674..596986c85a15be577355d4376e7c8094a934efb8 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.base_logic.lib Require Import invariants.
 From iris.proofmode Require Import tactics.
 From iris.bi Require Import fractional.
@@ -368,9 +367,9 @@ Section ArcGhost.
     iDestruct (@own_valid _ arcUR with "WU")
       as %[_ [_ [[VAL _]%auth_frag_valid_1 _]]].
     iPureIntro. simpl in VAL.
-    have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
-    apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
-    eapply Qclt_le_trans; [apply Lt|done].
+    have Lt: (1 < 1 + q)%Qp. apply Qp_lt_sum. by eexists.
+    apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
+    eapply Qp_lt_le_trans; [apply Lt|done].
   Qed.
 
   Lemma WkUps_update γ Ut1 Ut2 Ut' q :
@@ -441,19 +440,18 @@ Section ArcGhost.
 
   Lemma StrongAuth_new_tok γ (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
     StrongAuth γ (Some (q,n)) ==∗
-    StrongAuth γ (Some ((q + (q'/2)%Qp)%Qp, (n + 1)%positive)) ∗
+    StrongAuth γ (Some ((q + q'/2)%Qp, (n + 1)%positive)) ∗
     StrongTok γ (q'/2)%Qp.
   Proof.
     iIntros "own". rewrite -embed_sep -own_op.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
     apply prod_update; simpl; [|by rewrite right_id].
     apply prod_update; simpl; [|done]. apply auth_update_alloc.
-    rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /= -frac_op' pair_op Some_op.
+    rewrite Pos.add_comm Qp_add_comm -pos_op_plus /= -frac_op' pair_op Some_op.
     rewrite -{2}(right_id None op (Some ((q' /2)%Qp, _))).
     apply op_local_update_discrete => _ /=. split; simpl; [|done].
     apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
-    apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
-    apply Qcplus_le_mono_r, Qp_ge_0.
+    apply Qp_add_le_mono_l. apply Qp_le_add_r.
   Qed.
 
   Lemma WeakAuth_first_tok γ iS :
@@ -470,7 +468,7 @@ Section ArcGhost.
 
   Lemma WeakAuth_new_tok γ iS (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
     WeakAuth γ (iS, Some (Cinl (q, n))) ==∗
-    WeakAuth γ (iS, Some (Cinl ((q + (q'/2)%Qp)%Qp, (n + 1)%positive))) ∗
+    WeakAuth γ (iS, Some (Cinl ((q + q'/2)%Qp, (n + 1)%positive))) ∗
     WeakTok γ (q'/2)%Qp.
   Proof.
     iIntros "own". rewrite -embed_sep -own_op.
@@ -478,13 +476,12 @@ Section ArcGhost.
     apply prod_update; simpl; [|by rewrite right_id].
     apply prod_update; simpl; [done|]. apply auth_update_alloc.
     apply prod_local_update; simpl; [done|].
-    rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /=
+    rewrite Pos.add_comm Qp_add_comm -pos_op_plus /=
             -frac_op' pair_op Cinl_op Some_op.
     rewrite -{2}(right_id None op (Some $ Cinl ((q' /2)%Qp, _))).
     apply op_local_update_discrete => _ /=. split; simpl; [|done].
     apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
-    apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
-    apply Qcplus_le_mono_r, Qp_ge_0.
+    apply Qp_add_le_mono_l. apply Qp_le_add_r.
   Qed.
 
   Lemma StrongAuth_drop_last γ q:
@@ -572,9 +569,9 @@ Section ArcGhost.
     iDestruct (@own_valid _ arcUR with "own") as %[[_ VAL] _]. simpl in VAL.
     iPureIntro. move : VAL. rewrite -auth_frag_op -pair_op -Some_op frac_op'.
     move => /auth_frag_valid /= [/= ? _].
-    have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
-    apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
-    eapply Qclt_le_trans; [apply Lt|done].
+    have Lt: (1 < 1 + q)%Qp. apply Qp_lt_sum. by eexists.
+    apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
+    eapply Qp_lt_le_trans; [apply Lt|done].
   Qed.
 
   Lemma StrMoves_full_exclusive γ q Mt' :
@@ -585,9 +582,9 @@ Section ArcGhost.
     iDestruct (StrMoves_fractional with "[$SM $SM']") as "SM".
     iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _]%auth_frag_valid_1 _] _] _]].
     iPureIntro. simpl in VAL.
-    have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
-    apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
-    eapply Qclt_le_trans; [apply Lt|done].
+    have Lt: (1 < 1 + q)%Qp. apply Qp_lt_sum. by eexists.
+    apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
+    eapply Qp_lt_le_trans; [apply Lt|done].
   Qed.
 
   Lemma WeakAuth_new_lock γ iS q:
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 59a4ce454092d8d7dc9233f97a27af592b97b482..b0fec12b97438bd7188f9a6922d10b417fd692c7 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.bi Require Import fractional.
 From iris.algebra Require Import frac.
@@ -16,25 +15,22 @@ Definition frac_bor `{!invG Σ, !lftG Lat E0 Σ, !frac_borG Σ} κ
     ▷ □ ⎡(∀ q1 q2, φ' (q1+q2)%Qp ↔ φ' q1 ∗ φ' q2) V0⎤  ∗
 
     (* Then we use an (internal) atomic persistent borrow. *)
-    &in_at{κ'} (∃ (qfresh : Qp) (qdep qused : Qc),
+    &in_at{κ'} (∃ (qfresh : Qp) (qdep qused : option Qp),
          (* We divide the 1 fraction into 3 parts... *)
-         ⌜0 ≤ qdep⌝%Qc ∗ ⌜0 ≤ qused⌝%Qc ∗ ⌜(qfresh + qdep + qused = 1)%Qc⌝ ∗
+         ⌜(qfresh ⋅? qdep ⋅? qused = 1)%Qp⌝ ∗
          (* First part: the piece of φ' which is still fresh. *)
          ⎡φ' qfresh V0⎤ ∗
          (* Second part: some tokens have been left in deposit while the
             fractured borrow is accessed. *)
-         (if decide (0 < qdep)%Qc is left H return _
-          then ⎡(mk_Qp qdep H).[κ'] V0⎤ else True) ∗
+         ⎡from_option (λ qdep', qdep'.[κ']) True qdep V0⎤ ∗
          (* Third part: the piece of φ' that is "already used". It can be given
             back when the lifetime ends, but cannot be used when accessing the
             fractured borrow.  *)
-         (if decide (0 < qused)%Qc is left H return _
-          then φ' (mk_Qp qused H) else True) ∗
+         from_option φ' True%I qused ∗
          (* We keep a set of "receipts", to prove that we will always have
             enough fractions of the lifetime in deposit. *)
-         (if decide (0 < qfresh+qused)%Qc is left H return _
-          then ⎡own γ (mk_Qp (qfresh+qused) H)⎤
-          else True (* Dummy, never happens *))))%I.
+         ⎡own γ (qfresh ⋅? qused)⎤))%I.
+
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
@@ -77,21 +73,18 @@ Section frac_bor.
         - iModIntro. iNext. iModIntro. iIntros (??).
           rewrite !bi.intuitionistically_elim. iApply ("Hfrac'" $! _ _).
         - by iApply (in_at_bor_share with "[Hφ]"). }
-      { iNext. iSplit. iDestruct "Hφ" as "[$ _]". iExists 1%Qp, 0, 0.
-        iDestruct "Hφ" as "[_ Hφ]". repeat (iSplit; [done|]).
-        rewrite /= -(proj2 (Qp_eq 1 (mk_Qp (1+0) _))) //. iFrame. }
+      { iNext. iSplit. iDestruct "Hφ" as "[$ _]". iExists 1%Qp, None, None; simpl.
+        iDestruct "Hφ" as "[_ Hφ]". repeat (iSplit; [done|]). by iFrame. }
       iIntros "!> Hφ H† !>". iNext.
-      iDestruct "Hφ" as (q q' q'' ?? Hsum) "(Hφ1 & Htok & Hφ2 & _)".
-      destruct (decide (0 < q')%Qc).
+      iDestruct "Hφ" as (q q' q'' Hsum) "(Hφ1 & Htok & Hφ2 & _)".
+      destruct q' as [q'|]; simplify_eq/=.
       { iExFalso. rewrite -(embed_pure False). iModIntro ⎡_⎤%I.
         iApply (lft_tok_dead_subj with "Htok [H†]"). iApply "H†". }
-      destruct (Qcle_lt_or_eq 0 q') as [|<-]; [done|done|].
-      rewrite Qcplus_0_r in Hsum. destruct (decide (0 < q'')%Qc).
+      destruct q'' as [q''|]; simplify_eq/=.
       { iDestruct ("Hfrac" with "[Hφ1 Hφ2]") as "H".
         - iSplitL "Hφ1"; [|done]. by iApply monPred_in_elim.
-        - by rewrite (proj2 (Qp_eq (q + mk_Qp q'' _) 1) Hsum). }
-      destruct (Qcle_lt_or_eq 0 q'') as [|<-]; [done|done|]. rewrite Qcplus_0_r in Hsum.
-      rewrite (proj2 (Qp_eq q 1) Hsum). by iApply monPred_in_elim.
+        - by iEval (rewrite -Hsum). }
+    by iApply monPred_in_elim.
     - iDestruct (monPred_in_intro with "Hfrac") as (V) "[HV Hfrac']".
       iDestruct "H" as (κ') "(#? & #? & >_)". iExists γ, κ', V, φ. iFrame "#".
       iSplitR; [|iSplitR].
@@ -111,7 +104,6 @@ Section frac_bor.
     ↑lftN ⊆ E →
     ⎡lft_ctx⎤ -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
-    assert (Inhabited Qc) by exact (populate 0%Qc).
     iIntros (?) "#LFT Hfrac Hκ".
     iDestruct "Hfrac" as (γ κ' V0 φ') "#(Hκκ' & HV0 & Hφ' & Hfrac & Hshr)".
     iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[Hκ Hclose]". done.
@@ -122,7 +114,7 @@ Section frac_bor.
     iDestruct (monPred_in_intro with "HH") as (V) "(#HV & H & %)".
     iAssert ⎡monPred_in Vb (Vb ⊔ V)⎤%I as "HVVb"; [solve_lat|].
     iDestruct ("H" with "HVVb")
-      as (qφ0 qtok qφ1) "(>% & >% & >% & Hφ0 & Htok' & Hφ1 & Hown)".
+      as (qφ0 qtok qφ1) "(>% & Hφ0 & >Htok' & Hφ1 & >Hown)".
     destruct (Qp_lower_bound (qκ'/2) (qφ0/2)) as (qq & qκ'0 & qφ0' & Hqκ' & Hqφ).
     iExists qq.
     iAssert (▷ φ qq ∗ ⎡▷ φ' (qφ0' + qφ0 / 2) V0⎤)%Qp%I with "[Hφ0]" as "[$ Hqφ]".
@@ -130,32 +122,20 @@ Section frac_bor.
       iDestruct ("Hfrac" with "Hφ0") as "[Hφ0 $]". iApply "Hφ'".
       by iApply (monPred_in_elim with "HV0"). }
     iAssert (▷ ⎡own γ qq⎤ ∗
-             ▷ if decide (0 < qφ0' + qφ0 / 2 + qφ1)%Qc is left H
-             then ⎡own γ (mk_Qp _ H)⎤ else True)%I with "[Hown]" as "[>Hown1 Hown2]".
-    { destruct (decide (0 < qφ0 + qφ1)%Qc) as [|[]]; last by apply Qcplus_pos_nonneg.
-      destruct decide as [|[]]; first last.
-      { assert (0 < / 2)%Qc by reflexivity. unfold Qcdiv.
-        auto using Qcplus_pos_nonneg, Qcplus_pos_pos, Qcmult_pos_pos. }
-      rewrite -bi.later_sep -embed_sep -own_op frac_op' monPred_at_embed. iNext.
-      rewrite [(_ + _)%Qp](_ : _ = {| Qp_car := qφ0 + qφ1 |}) //.
-      apply Qp_eq. apply Qp_eq in Hqφ. simpl in Hqφ.
-      rewrite /= !Qcplus_assoc -Hqφ (Qcplus_diag (qφ0/2)) Qcmult_div_r //. }
+             ▷ ⎡own γ (qφ0' + qφ0 / 2 ⋅? qφ1)%Qp⎤)%I with "[Hown]" as "[>Hown1 Hown2]".
+    { rewrite -bi.later_sep -embed_sep -own_op. iNext.
+      by rewrite -!frac_op' -!cmra_op_opM_assoc_L assoc_L !frac_op' -Hqφ Qp_div_2. }
     rewrite monPred_objectively_unfold Hqκ'. iDestruct ("Hκ2" $! V0) as "[Hκ2 Hκ2']".
     iMod ("Hclose'" with "[-Hown1 Hclose Hκ2']") as "Hκ1".
-    { iIntros "#HVb". iExists (qφ0' + qφ0 / 2)%Qp, (qtok + qq)%Qc, qφ1. iNext. iFrame.
-      iSplit; [|iSplit; [done|iSplit; [|iSplitR "Hφ1"]]].
-      - iPureIntro. apply Qcplus_nonneg_nonneg, Qclt_le_weak=>//.
-      - iPureIntro. simpl.
-        replace (qφ0' + qφ0 / 2%Z + (qtok + qq))%Qc
-          with (qq + qφ0' + qφ0 / 2%Z + qtok)%Qc by ring.
-        apply Qp_eq in Hqφ. simpl in Hqφ. rewrite -Hqφ Qcplus_diag Qcmult_div_r //.
-      - destruct (decide (0 < qtok)%Qc), (decide (0 < qtok + qq)%Qc)=>//.
-        + erewrite (proj2 (Qp_eq (mk_Qp (_ + _) _) (_ + qq))).
-          rewrite lft_tok_fractional monPred_at_embed. by iFrame "Htok'". done.
-        + destruct (Qcle_lt_or_eq 0 qtok) as [|<-]=>//.
-          erewrite (proj2 (Qp_eq (mk_Qp (_ + _) _) qq)). iFrame.
-          simpl. apply Qcplus_0_l.
-      - destruct (decide (0 < qφ1)%Qc); [|done]. iCombine "HV HVb" as "HH".
+    { iIntros "#HVb". iExists (qφ0' + qφ0 / 2)%Qp, (qtok ⋅ Some qq)%Qp, qφ1.
+      iNext. iFrame. iSplit; [|iSplitR "Hφ1"].
+      - iPureIntro.
+        rewrite (comm_L _ qtok) cmra_opM_opM_assoc_L -assoc_L Some_op_opM /=.
+        rewrite -cmra_op_opM_assoc_L frac_op' -(comm_L _ qq) assoc_L -Hqφ Qp_div_2.
+        by rewrite -cmra_opM_opM_assoc_L.
+      - rewrite comm_L Some_op_opM. destruct qtok as [qtok|]; simpl; [|done].
+        by iSplitL "Hκ2".
+      - destruct qφ1 as [qφ1|]; [|done]. iCombine "HV HVb" as "HH".
         iDestruct (monPred_in_intro with "HH") as (VV) "(HVV & % & %)".
         iApply (monPred_in_elim with "HVV"). iFrame. }
     rewrite -Hqκ'. iClear "Hκκ' HV HVVb". clear dependent qφ0' qtok qφ1 Vb qφ0 V.
@@ -165,47 +145,35 @@ Section frac_bor.
     iDestruct (monPred_in_intro with "HH") as (V) "(#HV & H & %)".
     iAssert ⎡monPred_in Vb (Vb ⊔ V)⎤%I as "HVVb"; [solve_lat|].
     iDestruct ("H" with "HVVb")
-      as (qφ0 qtok qφ1) "(>% & >% & >% & Hφ0 & Htok' & Hφ1 & Hown)".
-    destruct (decide (0 < qφ0 + qφ1)%Qc) as [|[]]; last by auto using Qcplus_pos_nonneg.
-    iClear "Hshr". rewrite monPred_at_embed. iDestruct "Hown" as ">Hown".
+      as (qφ0 qtok qφ1) "(>% & Hφ0 & >Htok' & Hφ1 & >Hown)".
+    iEval (rewrite -(Qp_div_2 qκ') {1}Hqκ').
+    iClear "Hshr".
     iCombine "Hown1" "Hown" as "Hown". iDestruct (own_valid with "Hown") as %Hval.
-    assert (qq + qφ0 + qφ1 ≤ 1)%Qc. {
-      destruct (decide (0 < qφ0 + qφ1)%Qc) as [|[]]; [|by apply Qcplus_pos_nonneg].
-      by rewrite -Qcplus_assoc. }
-    assert (0 ≤ qtok - qq)%Qc. {
-      replace (qtok - qq)%Qc with ((qφ0 + qtok + qφ1) - (qq + qφ0 + qφ1))%Qc by ring.
-      change 0%Qc with (1 - 1)%Qc. apply Qcplus_le_compat.
-        by apply reflexive_eq. by apply Qcopp_le_compat. }
-    replace qtok with (qtok - qq + qq)%Qc by ring.
-    destruct (decide (0 < qtok - qq + qq)%Qc) as [|[]]; last by apply Qcplus_nonneg_pos.
-    assert (∀ H,
-      (mk_Qp (qtok - qq + qq) H).[κ'] V0 ⊣⊢
-       (if decide (0 < qtok - qq)%Qc is left H return _ then (mk_Qp _ H).[κ'] V0 else True)
-       ∗ qq.[κ'] V0) as ->.
-    { intros ?. destruct (decide (0 < qtok - qq)%Qc) as [|EQ%Qcnot_lt_le%Qcle_antisym]=>//.
-      - rewrite -monPred_at_sep -lft_tok_fractional. by erewrite (proj2 (Qp_eq _ _)).
-      - erewrite (proj2 (Qp_eq _ _)), (left_id _ _)=>//=. by rewrite -EQ Qcplus_0_l. }
-    iDestruct "Htok'" as "[Htok1 >Htok2]". iCombine "Htok2" "Hκ2'" as "Htok2".
-    rewrite -monPred_at_sep -lft_tok_fractional -Hqκ'.
+    destruct qtok as [qtok|]; simplify_eq/=; last first.
+    { destruct (Qp_not_add_le_r qq 1). by rewrite {1}(_ : 1 = qφ0 ⋅? qφ1)%Qp. }
+    assert (∃ qm, qtok = qq ⋅? qm)%Qp as [qm ->].
+    { assert (qq ≤ qtok)%Qp as [[qm ->]%Qp_lt_sum| ->]%Qp_le_lteq.
+      - rewrite (Qp_add_le_mono_r _ _ (qφ0 ⋅? qφ1)). trans 1%Qp; [done|].
+        apply reflexive_eq. by rewrite -frac_op' -cmra_op_opM_assoc_L comm_L.
+      - by exists (Some qm).
+      - by exists None. }
+    iAssert (⎡from_option (λ qm', qm'.[κ']) True qm V0⎤ ∗ ⎡ monPred_at qq.[κ'] V0 ⎤)%I
+      with "[Htok']" as "[Htok1 Htok2]".
+    { destruct qm as [qm|]; simplify_eq/=; [|by auto].
+      iDestruct "Htok'" as "[$$]". }
+    iCombine "Htok2 Hκ2'" as "Htok2"; rewrite -monPred_at_sep -lft_tok_fractional.
     iDestruct (monPred_in_elim with "HV0 Htok2") as "$".
-    iApply "Hclose'". iIntros "#HVb". iExists qφ0, (qtok - qq)%Qc, (qφ1 + qq)%Qc.
-    replace (qφ0 + (qtok - qq) + (qφ1 + qq))%Qc with (qφ0 + qtok + qφ1)%Qc by ring.
-    iNext. iFrame "Hφ0 %". iSplit; [|iSplitL "Htok1"; [|iSplitR "Hown"]].
-    - iPureIntro. apply Qcplus_nonneg_nonneg, Qclt_le_weak=>//.
-    - by destruct (decide (0 < qtok - qq))%Qc.
-    - destruct (decide (0 < qφ1 + qq))%Qc as [|[]]; last by apply Qcplus_nonneg_pos.
-      destruct (decide (0 < qφ1)%Qc) as [|<-%Qcnot_lt_le%Qcle_antisym]=>//.
-      + erewrite (proj2 (Qp_eq (mk_Qp (_ + _) _) _)).
-        * rewrite !bi.intuitionistically_elim.
-          iDestruct (monPred_in_elim with "HV0 Hfrac") as "Hfrac'".
-          iApply "Hfrac'". iSplitL "Hφ"; [by iApply "Hφ'"|]. iCombine "HV HVb" as "HH".
-          iDestruct (monPred_in_intro with "HH") as (VV) "(HVV & % & %)".
-          iApply (monPred_in_elim with "HVV"). iFrame.
-        * simpl. ring.
-      + erewrite (proj2 (Qp_eq (mk_Qp _ _) qq)). by iApply "Hφ'". simpl; ring.
-    - destruct decide as [|[]].
-      + erewrite ->(proj2 (Qp_eq _ _)). iFrame. simpl. ring.
-      + auto using Qcplus_pos_pos, Qcplus_nonneg_pos.
+    iApply "Hclose'". iIntros "#HVb". iExists qφ0, qm, (Some (qq ⋅? qφ1)); simpl.
+    iNext. iFrame "Hφ0 %". iSplit; [|iSplitL "Htok1"; [done|iSplitR "Hown"]].
+    - iPureIntro. by rewrite -cmra_op_opM_assoc_L -(comm_L _ qq)
+        -cmra_op_opM_assoc_L (comm_L _ qq) cmra_op_opM_assoc_L.
+    - destruct qφ1 as [qφ1|]; simpl; [|by iApply "Hφ'"].
+      rewrite !bi.intuitionistically_elim.
+      iDestruct (monPred_in_elim with "HV0 Hfrac") as "Hfrac'".
+      iApply "Hfrac'". iSplitL "Hφ"; [by iApply "Hφ'"|]. iCombine "HV HVb" as "HH".
+      iDestruct (monPred_in_intro with "HH") as (VV) "(HVV & % & %)".
+      iApply (monPred_in_elim with "HVV"). iFrame.
+    - by rewrite -cmra_op_opM_assoc_L -(comm_L _ qq) cmra_op_opM_assoc_L.
   Qed.
 
   Lemma frac_bor_shorten φ κ κ' : κ ⊑ κ' -∗ &frac{κ'}φ -∗ &frac{κ}φ.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 802638e602533a64cc01978e7d746c17b127492c..782dd346c9425d5af31646bd050faa4bf3189e9d 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -276,7 +276,7 @@ Section typing.
       iMod (bor_create _ ϝ with "LFT Hκs") as "[Hκs HκsI]"; first done.
       iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
       { iApply (bor_fracture with "LFT Hκs"); [|done].
-        split; [by rewrite Qp_mult_1_r|]. apply _. }
+        split; [by rewrite Qp_mul_1_r|]. apply _. }
       iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
       + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
         iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 94937ba4e3f775aadd41fb1dd72511cc04733a10..663e1e214844559b57a18b7c74620a7d4e1048d5 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -1,5 +1,3 @@
-From Coq.QArith Require Import Qcanon.
-
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
@@ -202,7 +200,7 @@ Section arc.
         iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
         iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
         { iApply (bor_fracture with "LFT Hlft"); [|solve_ndisj].
-          constructor; [by rewrite Qp_mult_1_r|apply _]. }
+          constructor; [by rewrite Qp_mul_1_r|apply _]. }
         iExists _,_,_. iFrame "lc". iApply (bor_share with "Hrc"); solve_ndisj. }
       iMod ("Hclose1" with "[]"); [|done]. by auto.
     - iMod ("Hclose1" with "[]") as "_"; first by iRight; iNext.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 6fa28d522b125093d5e27d9ce8593afc2f6be205..86e8e3cc62f5049f2cfd2d649c37b8cd46ee2440 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -181,7 +181,7 @@ Section rc.
         iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
         iDestruct (frac_bor_lft_incl with "LFT [> Hlft]") as "$".
         { iApply (bor_fracture with "LFT Hlft");
-            [split; [by rewrite Qp_mult_1_r|apply _]|solve_ndisj]. }
+            [split; [by rewrite Qp_mul_1_r|apply _]|solve_ndisj]. }
         iApply (bor_na with "Hrc"); solve_ndisj. }
       iApply ("Hclose1" with "[]"). by auto.
     - iMod ("Hclose1" with "[]") as "_"; first by iRight.
@@ -593,9 +593,8 @@ Section code.
     iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
     { apply auth_update_alloc, prod_local_update_1,
       (op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
-      split; simpl; last done. apply frac_valid'. rewrite -H comm_L -{2}(Qp_div_2 qb).
-      apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
-      apply Qcplus_le_mono_r, Qp_ge_0. }
+      split; simpl; last done. apply frac_valid'. rewrite /= -H comm_L.
+      by apply Qp_add_le_mono_l, Qp_div_le. }
     rewrite right_id -Some_op -Cinl_op -pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
     iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
     iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok2 Hν† $Hna]") as "Hna".
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index eadb9ca551a6a12dc60649e1c91af06e1aea4e7c..210720639a03e8dd5289e3420bf247043b28a530 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree numbers.
 From lrust.lang Require Import memcpy.
@@ -175,9 +174,7 @@ Section code.
       { apply auth_update_alloc, prod_local_update_1,
         (op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
         split; simpl; last done. apply frac_valid'.
-        rewrite -Hq''q0 comm_L -{2}(Qp_div_2 qb).
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
-        apply Qcplus_le_mono_r, Qp_ge_0. }
+        rewrite /= -Hq''q0 comm_L. by apply Qp_add_le_mono_l, Qp_div_le. }
       rewrite right_id -Some_op -Cinl_op -pair_op.
       iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
       iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hν2 Hν† $Hna]") as "Hna".
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index d24833bfb619038c5a8334d34b68a83a41740260..4028a108c4cf002342581e5e00d8078af7396762 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -56,7 +56,7 @@ Section ref.
     iMod (bor_persistent with "LFT Hinv Htok") as "[#Hinv $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν Hb]". done.
     iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
-    { iApply bor_fracture; try done. split. by rewrite Qp_mult_1_r. apply _. }
+    { iApply bor_fracture; try done. split. by rewrite Qp_mul_1_r. apply _. }
     iMod (bor_na with "Hb") as "#Hb". done. eauto 20.
   Qed.
   Next Obligation.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index f8d64e9fc4e162694c8e468dd0b3ad75aae4a493..62f4a49f6b224f47df71435daa0dd3c148d7730b 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
@@ -12,7 +11,7 @@ Section ref_functions.
   Lemma refcell_inv_reading_inv tid l γ α ty q ν :
     refcell_inv tid l γ α ty -∗
     ⎡own γ (◯ reading_stR q ν)⎤ -∗
-    ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
+    ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qp⌝ ∗
             ⎡own γ (● (refcell_st_to_R $ Some (ν, false, q', n)) ⋅ ◯ reading_stR q ν)⎤ ∗
             ((1).[ν] ={↑lftN ∪ ↑histN}[↑histN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
@@ -20,7 +19,7 @@ Section ref_functions.
   Proof.
     iIntros "INV H◯".
     iDestruct "INV" as (st) "(H↦lrc & H● & INV)".
-    iAssert (∃ q' n, st ≡ Some (ν, false, q', n) ∗ ⌜q ≤ q'⌝%Qc)%I with
+    iAssert (∃ q' n, st ≡ Some (ν, false, q', n) ∗ ⌜q ≤ q'⌝%Qp)%I with
        "[#]" as (q' n) "[%%]".
     { destruct st as [[[[??]?]?]|];
       iDestruct (own_valid_2 with "H● H◯")
@@ -73,10 +72,9 @@ Section ref_functions.
          (op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
-        apply Qcplus_le_mono_r, Qp_ge_0. }
-    wp_apply wp_new; [done..|]. iIntros (lr) "(H†lr&Hlr)".
+      - apply frac_valid'. rewrite /= -Hq'q'' comm_L.
+        by apply Qp_add_le_mono_l, Qp_div_le. }
+    wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr)".
     iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
     wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
@@ -84,7 +82,7 @@ Section ref_functions.
     iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
     { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
       iFrame. iExists _. iFrame.
-      rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
+      rewrite (comm Qp_add) (assoc Qp_add) Qp_div_2 (comm Qp_add). auto. }
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
     iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
     iApply (type_type _ _ _
@@ -336,9 +334,8 @@ Section ref_functions.
          (op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite -Hq1q2 comm -{2}(Qp_div_2 q2).
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q2/2)%Qp).
-        apply Qcplus_le_mono_r, Qp_ge_0. }
+      - apply frac_valid'. rewrite /= -Hq1q2 comm_L.
+        by apply Qp_add_le_mono_l, Qp_div_le. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
@@ -350,7 +347,7 @@ Section ref_functions.
     iMod ("Hclosena" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
     { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
       iFrame. iExists _. iFrame.
-      rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
+      rewrite (comm Qp_add) (assoc Qp_add) Qp_div_2 (comm Qp_add). auto. }
     iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
     iApply (type_type _ [_] _ [ #lrefs ◁ box (Π[ref α ty1; ref α ty2]) ]
        with "[] LFT HE Hna HL Hk"); first last.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 81d8b73a3801226e9b12b0d796044eb45847d5c7..21e4ca17decdbcba89cfcfe61d2243873a2efdb8 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lang Require Import memcpy.
@@ -184,13 +183,12 @@ Section refcell_functions.
               (op_local_update_discrete _ _ (reading_stR (q'/2)%Qp ν)) => ?.
             split; [split|].
             - by rewrite /= agree_idemp.
-            - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
-              apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
-              apply Qcplus_le_mono_r, Qp_ge_0.
+            - apply frac_valid'. rewrite /= -Hqq' comm_L.
+              by apply Qp_add_le_mono_l, Qp_div_le.
             - done. }
           iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
           rewrite [_ ⋅ _]comm -Some_op -!pair_op agree_idemp. iFrame.
-          iExists _. iFrame. rewrite -(assoc Qp_plus) Qp_div_2 //.
+          iExists _. iFrame. rewrite -(assoc Qp_add) Qp_div_2 //.
         - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
           iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
             auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 3776c5e75e93959c19b05257c84a2b2a3fa5d461..6a2cecc462b0f0fe25e9faf33140443e23c2a577 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -55,7 +55,7 @@ Section refmut.
     iMod (bor_sep with "LFT H") as "[_ H]". done.
     iMod (bor_sep with "LFT H") as "[H _]". done.
     unshelve (iMod (bor_fracture _ (λ q, (q' * q).[ν])%I with "LFT H") as "H"=>//); try apply _; [|].
-    { split. by rewrite Qp_mult_1_r. apply _. }
+    { split. by rewrite Qp_mul_1_r. apply _. }
     iDestruct (frac_bor_lft_incl with "LFT H") as "#Hκν". iClear "H".
     iExists _, _. iFrame "H↦". iApply delay_sharing_nested; try done.
     rewrite -assoc. iApply lft_intersect_mono; first by iApply lft_incl_refl.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 57f781da73844ac668d92ddbb4b843e6b808cca3..424ab2ba1cb9914549e6d3f682bba88a007b3d16 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
@@ -81,7 +80,7 @@ Section refmut_functions.
     iMod (bor_sep with "LFT H") as "[_ H]". done.
     iMod (bor_sep with "LFT H") as "[H _]". done.
     unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; try done.
-    { split. by rewrite Qp_mult_1_r. apply _. }
+    { split. by rewrite Qp_mul_1_r. apply _. }
     iDestruct (frac_bor_lft_incl _ _ q with "LFT H") as "#Hαν". iClear "H".
     rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
@@ -308,9 +307,8 @@ Section refmut_functions.
          (op_local_update_discrete _ _ (writing_stR (q1/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite -Hqq1 comm -{2}(Qp_div_2 q1).
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q1/2)%Qp).
-        apply Qcplus_le_mono_r, Qp_ge_0. }
+      - apply frac_valid'. rewrite /= -Hqq1 comm_L.
+        by apply Qp_add_le_mono_l, Qp_div_le. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton /= freeable_sz_full.
@@ -323,7 +321,7 @@ Section refmut_functions.
     { iExists (Some (_, true, _, _)).
       rewrite -Some_op -!pair_op agree_idemp /= (comm _ xH _).
       iFrame. iSplitL; [|done]. iExists _. iFrame.
-      rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
+      rewrite (comm Qp_add) (assoc Qp_add) Qp_div_2 (comm Qp_add). auto. }
     iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
     iApply (type_type _ [_] _ [ #lrefmuts ◁ box (Π[refmut α ty1; refmut α ty2]) ]
        with "[] LFT HE Hna HL Hk"); first last.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index de3da62e791d565edee31bfd62baf35a28cb7984..d2cf24200e74cfafb3c5f5dc99c2a954235b9959 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth excl csum frac agree numbers.
@@ -71,15 +70,14 @@ Section rwlock_inv.
   Proof.
     iIntros (st') "g". rewrite -embed_sep -own_op.
     iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
-    rewrite Pos.add_comm Qp_plus_comm -pos_op_plus /=
+    rewrite Pos.add_comm Qp_add_comm -pos_op_plus /=
             -{2}(agree_idemp (to_agree _)) -frac_op'
             2!pair_op Cinr_op Some_op.
     rewrite -{2}(right_id None op (Some (Cinr (_, (q' /2)%Qp, _)))).
     apply op_local_update_discrete =>-[Hagv _]. split; [split|done].
     - by rewrite /= agree_idemp.
-    - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
-      apply Qcplus_le_mono_l. rewrite -{1}(Qcanon.Qcplus_0_l (q'/2)%Qp).
-      apply Qcplus_le_mono_r, Qp_ge_0.
+    - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q') /=.
+      apply Qp_add_le_mono_l. apply Qp_le_add_r.
   Qed.
 
   Lemma rwown_update_write γs :
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 17576c1b30a11b6aba1ae5630c9822c974f25f25..0e9e4c64091ec164992c47b4d4b880df824aad8d 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -259,7 +259,7 @@ Section rwlock_functions.
             by iFrame "Htok2 Hshr rst H† R1".
           + iExists (Some (inr (ν, (q + q' / 2)%Qp, (n + 1)%positive))).
             iSplitL ""; [done|]. iFrame "Share g W'". iExists _.
-            iFrame "H† Hh Hshr Htok1 R2". by rewrite -Qp_plus_assoc Qp_div_2.
+            iFrame "H† Hh Hshr Htok1 R2". by rewrite -Qp_add_assoc Qp_div_2.
         - rewrite Eqst2. iDestruct "INT" as "(Hown & $ & R)".
           iExists (). iSplitL ""; [done|]. iIntros (t2 Ext2) "W' !>". iSplitL "".
           { rewrite /Q1 Eqst2. by iIntros "!> $". } iIntros "!> !>".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 0469dc74c242bc77d5e51c9662b30e6ba83cef34..432dc93804a0aac60ad3d3f9db5d45de81b84e12 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -50,7 +50,7 @@ Section rwlockreadguard.
     iMod (bor_persistent with "LFT Hαβ Htok") as "[#Hαβ $]". done.
     iMod (bor_sep with "LFT Hb") as "[Hκν _]". done.
     iDestruct (frac_bor_lft_incl with "LFT [> Hκν]") as "#Hκν".
-    { iApply bor_fracture; try done. constructor; [by rewrite Qp_mult_1_r|apply _]. }
+    { iApply bor_fracture; try done. constructor; [by rewrite Qp_mul_1_r|apply _]. }
     iExists _. iFrame "#". iApply ty_shr_mono; last done.
     iApply lft_intersect_mono; last done. iApply lft_incl_refl.
   Qed.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index f76e7f02f3e66c0ec45c9dcc3dfad36985c6bf26..acb8d15d890fefa911485a6c135d406e3ca8520b 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree numbers.
@@ -133,14 +132,14 @@ Section rwlockreadguard_functions.
           iExists None. iSplitL ""; [done|]. iFrame "Share H● Hb W".
           iDestruct (GPS_SWSharedReaders_join with "R Rm") as "R".
           by rewrite Hqrq'.
-        - inversion Eqst as [Eqst1]. rewrite Eqn Qp_plus_comm Eqst1.
+        - inversion Eqst as [Eqst1]. rewrite Eqn Qp_add_comm Eqst1.
           iMod (rwown_update_read_dealloc with "H● H◯") as "H●".
           iApply step_fupd_intro; [solve_ndisj|]. iIntros "!>". iSplitL ""; [done|].
           have Eqn': (Z.pos n - 1) = Z.pos (Pos.pred n).
           { rewrite Pos2Z.inj_pred => // ?. by subst n. } rewrite Eqn'.
           iExists (Some (inr (ν, q0, Pos.pred n))). iSplitL ""; [done|].
           iFrame "Share H● W". iExists (q + qr)%Qp. iFrame "H† Hh Hshr Hν".
-          iSplitR "R Rm"; [by rewrite Qp_plus_assoc (Qp_plus_comm q0)|].
+          iSplitR "R Rm"; [by rewrite Qp_add_assoc (Qp_add_comm q0)|].
           by iApply (GPS_SWSharedReaders_join with "R Rm"). } }
 
     iIntros "!>" (b t [] v') "(Hβ & _ & CASE)".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 4c9a3ca3c51c0e0abdaea98bedb4176019621151..d2691c559e227120b32f1aafdb0274d9814574f1 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 03080ae65c8b0d0de2dfc28eb85eb8651f3170f1..7d53c63d82509dc2b384cb46dc4d7a833402a664 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
@@ -8,24 +7,24 @@ Set Default Proof Using "Type".
 Section own.
   Context `{!typeG Σ}.
 
-  Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
+  Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
     match sz, n return _ with
     | 0%nat, _ => True
     | _, 0%nat => False
-    | sz, n => †{mk_Qp (sz / n) _}l…sz
+    | sz, n => †{pos_to_Qp (Pos.of_nat sz) / pos_to_Qp (Pos.of_nat n)}l…sz
     end%I.
-  Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
   Arguments freeable_sz : simpl never.
-  Global Instance freable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
+
+  Global Instance freeable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
 
   Lemma freeable_sz_full n l :
     ⎡freeable_sz n n l⎤%I ≡@{vProp _} (⎡†{1}l…n⎤ ∨ ⌜Z.of_nat n = 0⌝)%I.
   Proof.
-    destruct n.
+    destruct n as [|n].
     - iSplit; iIntros "H /="; auto.
     - assert (Z.of_nat (S n) = 0 ↔ False) as -> by done. rewrite right_id.
-      rewrite /freeable_sz (proj2 (Qp_eq (mk_Qp _ _) 1)) //= /Qcdiv Qcmult_inv_r //.
+      by rewrite /freeable_sz Qp_div_diag.
   Qed.
 
   Lemma freeable_sz_full_S n l : ⎡freeable_sz (S n) (S n) l⎤%I ≡@{vProp _} ⎡†{1}l…(S n)⎤%I.
@@ -39,8 +38,8 @@ Section own.
     - by rewrite left_id shift_loc_0.
     - by rewrite right_id Nat.add_0_r.
     - iSplit. by iIntros "[[]?]". by iIntros "[]".
-    - rewrite hist_freeable_op_eq. f_equiv. apply Qp_eq.
-      rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add /Qcdiv /=. do 3 f_equal. lia.
+    - rewrite hist_freeable_op_eq. f_equiv.
+      by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
   Qed.
 
   (* Make sure 'simpl' doesn't unfold. *)
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 4463e0d1ab5cc31b97ae8a83577af3a82debddcc..a28c87860de865c5b8222ba324649142a3468153 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
 From iris.algebra Require Import numbers.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 1adf126a059a3cd792438e5b6f596eec1185335b..6cbb1e3b3bef5d9e4f39a2fd1f81ea95423e517a 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".