diff --git a/restructuring/analysis/basic_facts/all.v b/restructuring/analysis/basic_facts/all.v
new file mode 100644
index 0000000000000000000000000000000000000000..96e03e8710a9764d55816336bc1f70be578647e1
--- /dev/null
+++ b/restructuring/analysis/basic_facts/all.v
@@ -0,0 +1,6 @@
+Require Export rt.restructuring.analysis.basic_facts.service.
+Require Export rt.restructuring.analysis.basic_facts.completion.
+Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
+Require Export rt.restructuring.analysis.basic_facts.sequential.
+Require Export rt.restructuring.analysis.basic_facts.arrivals.
+Require Export rt.restructuring.analysis.basic_facts.deadlines.
diff --git a/restructuring/behavior/facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
similarity index 100%
rename from restructuring/behavior/facts/arrivals.v
rename to restructuring/analysis/basic_facts/arrivals.v
diff --git a/restructuring/behavior/facts/completion.v b/restructuring/analysis/basic_facts/completion.v
similarity index 99%
rename from restructuring/behavior/facts/completion.v
rename to restructuring/analysis/basic_facts/completion.v
index 7743faeb4048dcf073dcbbf31a16b1d2592efba9..582c4d82953880b8f5aa9efa5a74fe140e3028fc 100644
--- a/restructuring/behavior/facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,5 +1,5 @@
 From rt.restructuring.behavior Require Export schedule.
-From rt.restructuring.behavior.facts Require Export service.
+From rt.restructuring.analysis.basic_facts Require Export service.
 
 From rt.util Require Import nat.
 
diff --git a/restructuring/behavior/facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
similarity index 94%
rename from restructuring/behavior/facts/deadlines.v
rename to restructuring/analysis/basic_facts/deadlines.v
index 703f5529c27cfea6cab10ec891b7a0cf08824fb4..1196bd3e3e328e82c10f8be6308c3b237aeed632 100644
--- a/restructuring/behavior/facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -1,4 +1,5 @@
-From rt.restructuring.behavior Require Export schedule facts.service facts.completion.
+From rt.restructuring.behavior Require Export schedule.
+From rt.restructuring.analysis.basic_facts Require Export service completion.
 
 (** In this file, we observe basic properties of the behavioral job
     model w.r.t. deadlines. *)
@@ -69,4 +70,4 @@ Section DeadlineFacts.
 
   End EqualProgress.
 
-End DeadlineFacts.
\ No newline at end of file
+End DeadlineFacts.
diff --git a/restructuring/behavior/facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
similarity index 100%
rename from restructuring/behavior/facts/ideal_schedule.v
rename to restructuring/analysis/basic_facts/ideal_schedule.v
diff --git a/restructuring/behavior/facts/sequential.v b/restructuring/analysis/basic_facts/sequential.v
similarity index 100%
rename from restructuring/behavior/facts/sequential.v
rename to restructuring/analysis/basic_facts/sequential.v
diff --git a/restructuring/behavior/facts/service.v b/restructuring/analysis/basic_facts/service.v
similarity index 100%
rename from restructuring/behavior/facts/service.v
rename to restructuring/analysis/basic_facts/service.v
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 5bb6e8b7283c1be6dd0662e4412215fb68f729fe..7226af67427d5305edee46f132893562b7a838be 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -1,5 +1,6 @@
-From rt.restructuring.behavior Require Export schedule facts.completion.
+From rt.restructuring.behavior Require Export schedule.
 From rt.restructuring.model Require Export task.
+From rt.restructuring.analysis.basic_facts Require Export completion.
 From rt.util Require Export seqset.
 
 Section Task.
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/transform/facts/edf_opt.v
index 28cc99010938d0d094dfcba18c5d1f0e4daf0e98..c298caee9f8d08c62fe69fb7cc04e9312299697f 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/transform/facts/edf_opt.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Export facts.all.
+From rt.restructuring.analysis Require Export basic_facts.all.
 From rt.restructuring.model Require Export schedule.edf.
 From rt.restructuring.analysis Require Export schedulability transform.edf_trans transform.facts.swaps.
 
diff --git a/restructuring/analysis/transform/facts/replace_at.v b/restructuring/analysis/transform/facts/replace_at.v
index 4c16fe2fa8f6f85c4665a5e2e4a9085f9c906e59..62c52ec27c855324db658ead963f33bc1b3ca909 100644
--- a/restructuring/analysis/transform/facts/replace_at.v
+++ b/restructuring/analysis/transform/facts/replace_at.v
@@ -1,5 +1,5 @@
 From rt.restructuring.analysis.transform Require Export swap.
-From rt.restructuring.behavior.facts Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
 From rt.util Require Import nat.
 
 (** In this file, we make a few simple observations about schedules with
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/transform/facts/swaps.v
index 1535a6a9ac45e138aacf42a535e9f637c96401bf..5395156ae9fdab7310b6e3cf1da6d0a37cd942e2 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/transform/facts/swaps.v
@@ -1,5 +1,5 @@
 From rt.restructuring.analysis.transform Require Export swap facts.replace_at.
-From rt.restructuring.behavior.facts Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
 From rt.util Require Import nat.
 
 (** In this file, we establish invariants about schedules in which two
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index e67da6b8f918da8b4de601595effdbd41e905e94..2187ebe2a50c4baf1e5c029475f7d073d52a691e 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import ssrnat ssrbool fintype.
-From rt.restructuring.behavior Require Import schedule facts.all.
+From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.analysis Require Import basic_facts.all.
 
 (** This file provides an operation that transforms a finite prefix of
     a given schedule by applying a point-wise transformation to each
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index 1cd62f9e1290463d69dad713c793d525df3ff00c..6f32fc7d364101417713597bcb23ac69171c86d3 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -1,5 +1,5 @@
 From rt.restructuring.behavior Require Export schedule job.
-From rt.restructuring.behavior.facts Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
 
 (** This file defines simple allocation substitutions and a swapping operation
     as used for instance in the classic EDF optimality proof. *)
diff --git a/restructuring/behavior/facts/all.v b/restructuring/behavior/facts/all.v
deleted file mode 100644
index ef6afe004cae1128d9ea91eb3a4f9f1d72b8de4e..0000000000000000000000000000000000000000
--- a/restructuring/behavior/facts/all.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Require Export rt.restructuring.behavior.facts.service.
-Require Export rt.restructuring.behavior.facts.completion.
-Require Export rt.restructuring.behavior.facts.ideal_schedule.
-Require Export rt.restructuring.behavior.facts.sequential.
-Require Export rt.restructuring.behavior.facts.arrivals.
-Require Export rt.restructuring.behavior.facts.deadlines.
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index d9fd6d8602da58cc7cbae418ffcbe8a022d648bc..2852f526a9b916e7895d3f416211e6296c7ee369 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -1,5 +1,5 @@
 From rt.restructuring.behavior Require Export schedule.
-From rt.restructuring.behavior.facts Require Import completion.
+From rt.restructuring.analysis.basic_facts Require Import completion.
 
 (* We define the readiness indicator function for the classic Liu & Layland
    model without jitter and no self-suspensions, where jobs are always
diff --git a/restructuring/model/schedule/task_schedule.v b/restructuring/model/schedule/task_schedule.v
index 97c6a111e25b91a11f0271d085e0389cec5c326d..0a5ef66ec6862d1cdcce23b7fee0bc1e3a4dbe8f 100644
--- a/restructuring/model/schedule/task_schedule.v
+++ b/restructuring/model/schedule/task_schedule.v
@@ -1,5 +1,6 @@
 From rt.restructuring.model Require Import task.
-From rt.restructuring.behavior Require Import schedule ideal_schedule.
+From rt.restructuring.behavior Require Import schedule.
+From rt.restructuring.analysis.basic_facts Require Import ideal_schedule.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
@@ -49,4 +50,4 @@ Section ScheduleOfTask.
 
   End TaskProperties.
 
-End ScheduleOfTask. 
\ No newline at end of file
+End ScheduleOfTask.