diff --git a/opam b/opam
index 35a8ce26c61af2d539e56f65cb591e433505b133..a12c3e4ff785b7797824d43d2105e5df27290b8c 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-10-15.2.f4060bb5") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-30.0.6dba10c0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 5ec249ec25572159055eef28cdea9b79cb77c6fe..90d563baab5779278648fe4f835eeef695881b1e 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -1,4 +1,3 @@
-From Coq.QArith Require Import Qcanon.
 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Import weakestpre.
 From iris.proofmode Require Import tactics.
@@ -275,9 +274,8 @@ Section arc.
       { apply auth_update_alloc, prod_local_update_1,
          (op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
            =>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
-        apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 qq).
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
-        apply Qcplus_le_mono_r, Qp_ge_0. }
+        apply frac_valid'. rewrite -Hq comm_L.
+        by apply Qp_add_le_mono_l, Qp_div_le. }
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
       iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
       { iExists _. iFrame. iExists _. rewrite /= [xH â‹… _]comm_L. iFrame.
@@ -407,9 +405,8 @@ Section arc.
           { apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
             apply op_local_update_discrete=>Hv. constructor; last done.
             split; last by rewrite /= left_id; apply Hv. split=>[|//].
-            apply frac_valid'. rewrite -Heq comm_L -{2}(Qp_div_2 q).
-            apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
-            apply Qcplus_le_mono_r, Qp_ge_0. }
+            apply frac_valid'. rewrite /= -Heq comm_L.
+            by apply Qp_add_le_mono_l, Qp_div_le. }
           iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
           rewrite /= [xH â‹… _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
                   Qp_div_2 left_id_L. auto with iFrame.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index cb7addfa1e4ec5be9920e26f7d35f9c5c4e37db8..b571f34e1ab31e74624dcb453190d71a3ad17e8c 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.
@@ -76,21 +75,16 @@ Section frac_bor.
     iIntros "#Hφ (H & Hown & Hφ1)". iNext.
     iDestruct "H" as (qφ) "(Hφqφ & Hown' & [%|Hq])".
     { subst. iCombine "Hown'" "Hown" as "Hown".
-      by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_ge. }
+      by iDestruct (own_valid with "Hown") as %Hval%Qp_not_add_le_l. }
     rewrite /frac_bor_inv. iApply bi.sep_exist_r. iExists (q + qφ)%Qp.
     iDestruct "Hq" as (q' Hqφq') "Hq'κ". iCombine "Hown'" "Hown" as "Hown".
     iDestruct (own_valid with "Hown") as %Hval. rewrite comm_L. iFrame "Hown".
     iCombine "Hφ1 Hφqφ" as "Hφq". iDestruct ("Hφ" with "Hφq") as "$".
-    assert (0 < q'-q ∨ q = q')%Qc as [Hq'q|<-].
-    { change (qφ + q ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'.
-      rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
-      destruct Hval as [Hval|Hval].
-      - left; apply ->Qclt_minus_iff. done.
-      - right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
-    - assert (q' = mk_Qp _ Hq'q + q)%Qp as ->. { apply Qp_eq. simpl. ring. }
-      iDestruct "Hq'κ" as "[Hq'qκ $]".
-      iRight. iExists _. iIntros "{$Hq'qκ}!%".
-      revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring.
+    assert (q ≤ q')%Qp as [[r ->]%Qp_lt_sum|<-]%Qp_le_lteq.
+    { apply (Qp_add_le_mono_l _ _ qφ). by rewrite Hqφq'. }
+    - iDestruct "Hq'κ" as "[$ Hr]".
+      iRight. iExists _. iIntros "{$Hr} !%".
+      by rewrite (comm_L Qp_add q) -assoc_L.
     - iFrame "Hq'κ". iLeft. iPureIntro. rewrite comm_L. done.
   Qed.
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 1dd2d629f03ef6b86ff1034bc21868e8a0680651..607a0960a2170debc2e4de36d83b4c625284d640 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -271,7 +271,7 @@ Section typing.
       iSpecialize ("Hf" $! x ϝ _ vl). iDestruct (HE ϝ with "HL") as "#HE'".
       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"); first done. by rewrite Qp_mult_1_r. }
+      { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mul_1_r. }
       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 b7ac9370e30149c69221cf8b516ee132805984ce..95ed3014e4526b3cab8beed6dc2da1b59b5c5bf7 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.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.
 From iris.bi Require Import fractional.
@@ -142,7 +141,7 @@ Section arc.
       { iExists _, _, _. iFrame "Hpersist".
         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"); first solve_ndisj. by rewrite Qp_mult_1_r. }
+        { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mul_1_r. }
         iApply (bor_share with "Hrc"); solve_ndisj. }
       iApply ("Hclose1" with "[]"). by auto.
     - iMod ("Hclose1" with "[]") as "_"; first by auto.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 72e08c6d60fa19549f023ade400572bbe30a0fd8..cf3f8f6b244eff1b05c283120a911a136caeb05f 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.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.
 From lrust.lang.lib Require Import memcpy lock.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index cbd04b88f7c320a29d74b4f4c5a7806bc5036d80..25fbede9afb92d6c7b3d4f586dea638e8efee81a 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.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.
 From lrust.lang.lib Require Import memcpy lock.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 6f720ade7335a78796540a0f3034fa7829870401..81ad0634679d86a37fbb8c0ea2297767ac2f9ce6 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.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 excl numbers.
 From lrust.lang.lib Require Import memcpy.
@@ -175,7 +174,7 @@ Section rc.
       { iExists _, _, _. iFrame "Hpersist".
         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"); first solve_ndisj. by rewrite Qp_mult_1_r. }
+        { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mul_1_r. }
         iApply (bor_na with "Hrc"); solve_ndisj. }
       iApply ("Hclose1" with "[]"). by auto.
     - iMod ("Hclose1" with "[]") as "_"; first by auto.
@@ -591,9 +590,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 5d61d108714bcc88986c4b3bc78f85ee788cc0b1..987eb1b9e4e194bd57b28228d876c27ef2aec050 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.lib Require Import memcpy.
@@ -169,9 +168,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 108291c45bf33f41bbe42633acd5ca962f0645d7..87cd76a52c6cafb6409a414288fa16dfef187591 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -57,7 +57,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. by rewrite Qp_mult_1_r. }
+    { iApply bor_fracture; try done. by rewrite Qp_mul_1_r. }
     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 9a2bb7026e55b7221cf7bf2edeaa8ddaad37efc1..bf9ac8b1e12b305e4f95d7718b67079f4d317a8f 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.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
@@ -13,7 +12,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 ∪ ↑lft_userN}[↑lft_userN]▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             (∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν]) ∗
@@ -21,7 +20,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◯")
@@ -74,9 +73,8 @@ 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. }
+      - 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. }
@@ -85,7 +83,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 _ _ _
@@ -337,9 +335,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.
@@ -351,7 +348,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 70979851be15379f04aea93af6ce578cfe7e2852..6bda8af9ade8049703a2260056c41c152660ba19 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.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
@@ -185,13 +184,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 4c92b64da7ad6d1fc17985c69fc743c0e884a5a4..8d2978ff505c66dcc2b01c0b6312c65314418582 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -56,7 +56,7 @@ Section refmut.
     iMod (bor_sep with "LFT H") as "[_ H]". done.
     iMod (bor_sep with "LFT H") as "[H _]". done.
     iMod (bor_fracture (λ q, (q' * q).[ν])%I with "LFT [H]") as "H". done.
-    { by rewrite Qp_mult_1_r. }
+    { by rewrite Qp_mul_1_r. }
     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 69b894f174bb8751dddbda931396ba9af4f518a4..25ade67a3f5213222ab53e7812623d4a27ea7545 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.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
@@ -82,7 +81,7 @@ Section refmut_functions.
     iMod (bor_sep with "LFT H") as "[_ H]". done.
     iMod (bor_sep with "LFT H") as "[H _]". done.
     iMod (bor_fracture (λ q', (q * q').[ν])%I with "LFT [H]") as "H". done.
-    { by rewrite Qp_mult_1_r. }
+    { by rewrite Qp_mul_1_r. }
     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.
@@ -310,9 +309,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.
@@ -325,7 +323,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_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index f0b3ac79e6693155ca886397df37fc637b9f0444..c3fbbc3835bb1fdaa700b8e5ef1bd1f0c48dc441 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.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.
 From iris.bi Require Import fractional.
@@ -194,13 +193,12 @@ Section rwlock_functions.
               (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
               split; [split|].
               - by rewrite /= Hag 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 _. rewrite Z.add_comm /=. iFrame. iExists _, _.
             iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
-            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 (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". solve_ndisj.
             iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
               auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 8cc6561c4c25560bb3b43a58ef394cadcf54d272..9dd3999a079898955ced24d72fe84074cb815315 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 Hinv Htok") as "[#Hinv $]". 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. by rewrite Qp_mult_1_r. }
+    { iApply bor_fracture; try done. by rewrite Qp_mul_1_r. }
     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 303ab8dd557c86de8c9f05a9ae8729bd28155f41..83babbae96ef1a3b2f0e014f957a943fda53b720 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.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 7aa33fb350d9d45831cf6a684dd890bf1d279bdf..df2411164125de173edc2ddd1813207c42dce71d 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.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index de9046c586795650d394acb9017dcd62bbe6144a..a4073bfb57ce0511c9f0334ede4b860d5165163e 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.lib Require Import memcpy.
 From lrust.typing Require Export type.
@@ -8,23 +7,23 @@ 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 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 ⊣⊢ †{1}l…n ∨ ⌜Z.of_nat n = 0⌝.
   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 ⊣⊢ †{1}l…(S n).
@@ -38,8 +37,8 @@ Section own.
     - by rewrite left_id shift_loc_0.
     - by rewrite right_id Nat.add_0_r.
     - iSplit. by iIntros "[[]?]". by iIntros "[]".
-    - rewrite heap_freeable_op_eq. f_equiv. apply Qp_eq; simpl.
-      by rewrite -Qcmult_plus_distr_l -Nat.add_succ_l Nat2Z.inj_add -Z2Qc_inj_add.
+    - rewrite heap_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 3dab3ddc3a31b41d2ffd02342ef8df8047652637..7a6344d705c1b19d1ea1bc8efbbc3defdaf0e38e 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -1,4 +1,3 @@
-From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".