diff --git a/_CoqProject b/_CoqProject
index 4a568257d95d8001c605b56eebbfae409513e024..e361d046c6f0f50b7d7a623f5ed4d87e59fb559a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,8 +17,6 @@ theories/algebra/big_op.v
 theories/algebra/cmra_big_op.v
 theories/algebra/sts.v
 theories/algebra/auth.v
-theories/algebra/frac_auth.v
-theories/algebra/excl_auth.v
 theories/algebra/gmap.v
 theories/algebra/ofe.v
 theories/algebra/base.v
@@ -40,7 +38,9 @@ theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
 theories/algebra/namespace_map.v
-theories/algebra/ufrac_auth.v
+theories/algebra/lib/excl_auth.v
+theories/algebra/lib/frac_auth.v
+theories/algebra/lib/ufrac_auth.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v
diff --git a/theories/algebra/excl_auth.v b/theories/algebra/lib/excl_auth.v
similarity index 100%
rename from theories/algebra/excl_auth.v
rename to theories/algebra/lib/excl_auth.v
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/lib/frac_auth.v
similarity index 100%
rename from theories/algebra/frac_auth.v
rename to theories/algebra/lib/frac_auth.v
diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
similarity index 100%
rename from theories/algebra/ufrac_auth.v
rename to theories/algebra/lib/ufrac_auth.v
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 7b205e54be3c46473144e185551aa13765819c0c..bf478327ce38a2c1595c0a7453a7653ee004286c 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import excl_auth gmap agree.
+From iris.algebra Require Import lib.excl_auth gmap agree.
 From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 8dfe67e62b8a32288ec934ecf405a0447ea8d6da..1d0fd7083b8554902c43642666309549d43e7ccc 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac_auth auth.
+From iris.algebra Require Import lib.frac_auth auth.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 17469f957b0e5379aac27e30a4da33acb5612e4a..85109f320b5c57a53af92b9aab6edd89dadc0541 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics classes.
-From iris.algebra Require Import excl_auth.
+From iris.algebra Require Import lib.excl_auth.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.