diff --git a/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala b/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
deleted file mode 100644
index 236926c7494329667908a4b2d620316df256acec..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-package lisa.proven
-
-object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.mathematics.PeanoArithmetics.runningPeanoTheory) {
-  export lisa.proven.mathematics.PeanoArithmetics.*
-}
diff --git a/src/main/scala/lisa/proven/mathematics/Peano.scala b/src/main/scala/lisa/proven/peano_example/Peano.scala
similarity index 99%
rename from src/main/scala/lisa/proven/mathematics/Peano.scala
rename to src/main/scala/lisa/proven/peano_example/Peano.scala
index 78b3244ea950daf636386ed97399975ed72235ab..ca74d81554cd7e88723762491490418b85fa8886 100644
--- a/src/main/scala/lisa/proven/mathematics/Peano.scala
+++ b/src/main/scala/lisa/proven/peano_example/Peano.scala
@@ -1,17 +1,16 @@
-package lisa.proven.mathematics
+package lisa.proven.peano_example
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
-import lisa.proven.PeanoArithmeticsLibrary
 import lisa.proven.tactics.ProofTactics.*
 import lisa.utils.Helpers.{_, given}
 import lisa.utils.Library
 import lisa.utils.Printer
 
 object Peano {
-  export lisa.proven.PeanoArithmeticsLibrary.{*, given}
+  export PeanoArithmeticsLibrary.{*, given}
 
   /////////////////////////// OUTPUT CONTROL //////////////////////////
   given output: (String => Unit) = println
diff --git a/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala b/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala
similarity index 98%
rename from src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
rename to src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala
index 62801b59840057266e73800e2c8f7d47590cf1c9..03797ff243ab25f83cd4929a13e447d427abe8a1 100644
--- a/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
+++ b/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala
@@ -1,4 +1,4 @@
-package lisa.proven.mathematics
+package lisa.proven.peano_example
 
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
diff --git a/src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala b/src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ca4c98bfa20b0a969b1fbea9938556776976d0b8
--- /dev/null
+++ b/src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala
@@ -0,0 +1,5 @@
+package lisa.proven.peano_example
+
+object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.peano_example.PeanoArithmetics.runningPeanoTheory) {
+  export lisa.proven.peano_example.PeanoArithmetics.*
+}