diff --git a/tests/one_shot.v b/tests/one_shot.v
index 13b4e05aaef3fa9b9749cff8191b50fec1d2ca44..3de778074989ff8490913e049a2dee1ecb24d6b9 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl agree csum.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 40efb5efc3e972c6887bce976b8de1d1d4da568f..13230b72860e57a20aecb047bb4ed4f6c4f22069 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac agree csum.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index a01fafc469a8ce0a34a93f749c4b6b5366c451fa..96b2f643a536a9d8ce859d2697667a86bd451169 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics monpred.
 From iris.algebra Require Import frac.
+From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 3bcb256e3c37a2320ba33ff02897bed909320a86..33400023366de58f8760ab5d9077eb8433f58ce0 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export bi.
 From iris.algebra Require Import frac.
+From iris.bi Require Export bi.
 From iris.base_logic Require Export bi.
 From iris Require Import options.
 Import bi.bi base_logic.bi.uPred.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index d02ce530697f2199d52f6c924a832f6468d87a84..2d99ad3c102b90743203fdd22c20cde5a704038d 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -1,6 +1,6 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index a186d80b6fe81107f5a1a40ecb182a45174a5902..179153fb4ea64412236ef90f62586bc0cab09b35 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 lib.excl_auth gmap agree.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index f0b3719daab960d4571842c57e7329b714a3e9a0..1c8964fc37c5b69acc77777ab49a359c5349c135 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Export frac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Export frac.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index ccd4ac39cf70d7b97817fe6de67f40db9fb42ac0..558fae055067fa77d4a9d79f4ebef5cd46022e49 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import wsat.
 From iris Require Import options.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index ac6140a6602e0d055f987f85829de9e38da70035..b48e4b052fce981d92d475a99dd0bb558f4d3527 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,7 +1,7 @@
 From stdpp Require Export namespaces.
+From iris.algebra Require Import gmap_view namespace_map agree frac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import gmap_view namespace_map agree frac.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index 0632b0c24f6ce076358239442e0a486d7ccb28e5..49aba300bec00aaa0eacef2364b973f5d7c9c95f 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -1,8 +1,8 @@
 (** A simple "ghost variable" of arbitrary type with fractional ownership.
 Can be mutated when fully owned. *)
+From iris.algebra Require Import frac_agree.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac_agree.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index adff4f6eb0a06733e346c854757bbc8bc6f9323a..5fa9cd8d0d8889f74b6a5abd58f7bd744d9935c4 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -1,6 +1,6 @@
 From stdpp Require Export namespaces.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.base_logic.lib Require Import wsat.
 From iris Require Import options.
diff --git a/theories/base_logic/lib/mnat.v b/theories/base_logic/lib/mnat.v
index 9773e4fafcd3fa263d20171b60d75b275b416dab..36096f2bfd92098e9c68c8b7f824cc41d3cb6ed5 100644
--- a/theories/base_logic/lib/mnat.v
+++ b/theories/base_logic/lib/mnat.v
@@ -8,9 +8,9 @@ lower-bound at [m] imply that [m ≤ n], and [mnat_update], which allows to
 increase the auth element. At any time the auth nat can be "snapshotted" with
 [mnat_get_lb] to produce a persistent lower-bound proposition. *)
 
-From iris.proofmode Require Import tactics.
 From iris.algebra.lib Require Import mnat_auth.
 From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c991982418c605ceca2c0ca42c45c324447fdf58..65bb13da862e8513194f7703e772d9687cb82050 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 586725300a542731901700695a9c5a1babccb4a3..f9915ee2b357ecfbed07c2b0b593e07408a23768 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import agree.
+From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export own.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 30ceaa1108423c9b6fec4c7edfb2a3c76707cd7a..329ead42a5efea3f83a025b1782129b8450f21b7 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Export sts.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 020d584ae096cb40cbbe06b09d2a8d8999c71fa1..c64dcebcdb96e2f3fcba1871562f5dad402eec01 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap_view gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 8b443a61b35095e79a23e1f4f81ee662e8a5a329..1508ddcc1e2052307bf3ada13f8e30bdb5c32de0 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,6 +1,6 @@
 From stdpp Require Import finite.
-From iris.bi Require Import notation.
 From iris.algebra Require Export cmra updates.
+From iris.bi Require Import notation.
 From iris Require Import options.
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core.
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 52ec4bebf2dd7d0fab0891695108aac0bb37336b..434592fd931fdb3b7f0fe39e0c920aedc6a6bb00 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -1,5 +1,4 @@
 From iris.bi Require Import interface derived_connectives updates.
-From iris.algebra Require Export ofe.
 From iris Require Import options.
 
 Notation "P |- Q" := (P ⊢ Q)
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index fdeb3a982771514003b786b90575c8b3ae70b39d..671a8ae13784a2815e9ecb3691b4d968da1e18db 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export interface.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export interface.
 From iris Require Import options.
 
 Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 5227d08edd7f4512516cd7f93c08a9eb82bd9c4b..7941169a2a34c84619c7dd92e2db8f66ebef5120 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export derived_connectives.
 From iris Require Import options.
 
 (* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index a683467de724d154d0e9fc20e20c22eba4df1cec..03d950b194f8f5925392ede9520c0380941a0898 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export derived_laws.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export derived_laws.
 From iris Require Import options.
 
 Module bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 4a70ddb3b2027ca569efd5067e2141cf429f9a30..bb73cf16aff25a4fce9395006c53d5d532f4ee2e 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Import monoid.
 From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
-From iris.algebra Require Import monoid.
 From iris Require Import options.
 
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ba41b1898570fbaa64b031603b60e1da6a7271fb..dc7155fb2107c40fb631f7bf13524d146a542071 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export notation.
 From iris.algebra Require Export ofe.
+From iris.bi Require Export notation.
 From iris Require Import options.
 Set Primitive Projections.
 
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 756dba593fd955d1b4067b4da66f758d15af765c..29ee3437dc9655479ddeb63f70ceca2589d49b12 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,5 +1,5 @@
-From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.algebra Require Import monoid.
+From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 7ffc5a931c5d5409556ff25da5251dda12c436e7..1c66662702103c87e544257ff24143b9563d657b 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
 From iris Require Import options.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 72109448c0034331d3cc1318bdcfb97da3164701..48537d024b8dd3b26a95d3055bcb2bcbc61d8308 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 lib.frac_auth numbers auth.
+From iris.proofmode Require Import tactics.
 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/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 9b10f92472869c843437e1be3b9f97258c6f5f32..0d033c5d1079ea5b8e266f27d3b965c54b916afc 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
+From iris.proofmode Require Import tactics.
 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/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 1e5af4e7310de9c20b5c0c587799196ec5d57bd6..8f4986496c807a4cd75a824dd95079590a0f2079 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 850db347dbc634cdf2b8fce87b8bc69d1d2bb16b..5b202eaed32f998c5b48d80cf83e6d491486c7cc 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl auth gset.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index afb76b7dbb5aca8d66c8e01465ae8576759c5cbe..5e1ccb1e6eb14f5ec155fed82809002243ac3ead 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -2,8 +2,8 @@
 the Iris lifting lemmas. *)
 
 From stdpp Require Import fin_maps.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
+From iris.proofmode Require Import tactics.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index fc3abc68ca672391c6cb66da6e151a86ccefd4a0..309857a216799ba46ebed2241d45530fc8c65773 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import wsat.
 From iris.program_logic Require Export weakestpre.
 From iris Require Import options.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 2a0fde9be9cfb4750221ddb65cf8fa66356e59e4..78e6ffcf9bdc044edb08677675c277bf42f4fc3f 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 lib.excl_auth.
+From iris.proofmode Require Import tactics classes.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 731f690798d8411b479846f275fea521d7dfd027..1825b3cd9779245e1de2c2f0e3c3c590c4b1998e 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.bi Require Import big_op fixpoint.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.program_logic Require Export total_weakestpre adequacy.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index b37062dc851953bc8efb739da6330397684c2df3..e77b6b44eff752ee9062629c38aed7470aa7e9ff 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Export base.
 From iris.bi Require Export bi.
 From iris.proofmode Require Import base.
-From iris.algebra Require Export base.
 From iris Require Import options.
 Import bi.