diff --git a/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala b/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
new file mode 100644
index 0000000000000000000000000000000000000000..236926c7494329667908a4b2d620316df256acec
--- /dev/null
+++ b/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
@@ -0,0 +1,5 @@
+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/mathematics/Peano.scala
index 2b6139ddd3ffc4dd988e9db45b215960facc26fc..48081a1968f25d665ab2f6db2e6f058d85993e8c 100644
--- a/src/main/scala/lisa/proven/mathematics/Peano.scala
+++ b/src/main/scala/lisa/proven/mathematics/Peano.scala
@@ -3,38 +3,14 @@ package lisa.proven.mathematics
 import lisa.utils.Helpers.{given, *}
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.proven.tactics.ProofTactics.*
+import lisa.proven.PeanoArithmeticsLibrary
+import lisa.utils.Helpers.{_, given}
+import lisa.utils.Library
 
 object Peano {
-  type Axiom = Formula
-  final val (x, y) =
-    (VariableLabel("x"), VariableLabel("y"))
-
-  final val zero: Term = ConstantFunctionLabel("0", 0)()
-  final val s = ConstantFunctionLabel("S", 1)
-  final val plus = ConstantFunctionLabel("+", 2)
-  final val times = ConstantFunctionLabel("*", 2)
-  final val sPhi: SchematicPredicateLabel = SchematicPredicateLabel("?p", 1)
-
-  final val ax1ZeroSuccessor: Axiom = forall(x, !(s(x) === zero))
-  final val ax2Injectivity: Axiom = forall(x, forall(y, (s(x) === s(y)) ==> (x === y)))
-  final val ax3neutral: Axiom = forall(x, plus(x, zero) === x)
-  final val ax4plus: Axiom = forall(x, forall(y, plus(x, s(y)) === s(plus(x, y))))
-  final val ax5: Axiom = forall(x, times(x, zero) === zero)
-  final val ax6: Axiom = forall(x, forall(y, times(x, s(y)) === plus(times(x, y), x)))
-  final val ax7induction: Axiom = (sPhi(zero) /\ forall(x, sPhi(x) ==> sPhi(s(x)))) ==> forall(x, sPhi(x))
-
-  final val runningPeanoTheory: RunningTheory = new RunningTheory()
-  final val functions: Set[ConstantFunctionLabel] = Set(ConstantFunctionLabel("0", 0), s, plus, times)
-  functions.foreach(runningPeanoTheory.addSymbol(_))
-
-  private val peanoAxioms: Set[(String, Axiom)] = Set(
-    ("A1", ax1ZeroSuccessor),
-    ("A2", ax2Injectivity),
-    ("A3", ax3neutral),
-    ("A4", ax4plus),
-    ("A5", ax5),
-    ("A6", ax6),
-    ("Induction", ax7induction)
-  )
-  peanoAxioms.foreach(a => runningPeanoTheory.addAxiom(a._1, a._2))
+  export lisa.proven.PeanoArithmeticsLibrary.{*, given}
+  given output: (String => Unit) = println
 }
diff --git a/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala b/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
new file mode 100644
index 0000000000000000000000000000000000000000..62801b59840057266e73800e2c8f7d47590cf1c9
--- /dev/null
+++ b/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
@@ -0,0 +1,39 @@
+package lisa.proven.mathematics
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.utils.Helpers.{_, given}
+
+object PeanoArithmetics {
+  final val (x, y, z) =
+    (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+
+  final val zero: Term = ConstantFunctionLabel("0", 0)()
+  final val s = ConstantFunctionLabel("S", 1)
+  final val plus = ConstantFunctionLabel("+", 2)
+  final val times = ConstantFunctionLabel("*", 2)
+  final val sPhi: SchematicPredicateLabel = SchematicNPredicateLabel("?p", 1)
+
+  final val ax1ZeroSuccessor: Formula = forall(x, !(s(x) === zero))
+  final val ax2Injectivity: Formula = forall(x, forall(y, (s(x) === s(y)) ==> (x === y)))
+  final val ax3neutral: Formula = forall(x, plus(x, zero) === x)
+  final val ax4plusSuccessor: Formula = forall(x, forall(y, plus(x, s(y)) === s(plus(x, y))))
+  final val ax5timesZero: Formula = forall(x, times(x, zero) === zero)
+  final val ax6timesDistrib: Formula = forall(x, forall(y, times(x, s(y)) === plus(times(x, y), x)))
+  final val ax7induction: Formula = (sPhi(zero) /\ forall(x, sPhi(x) ==> sPhi(s(x)))) ==> forall(x, sPhi(x))
+
+  final val runningPeanoTheory: RunningTheory = new RunningTheory()
+  final val functions: Set[ConstantFunctionLabel] = Set(ConstantFunctionLabel("0", 0), s, plus, times)
+  functions.foreach(runningPeanoTheory.addSymbol(_))
+
+  private val peanoAxioms: Set[(String, Formula)] = Set(
+    ("ax1ZeroSuccessor", ax1ZeroSuccessor),
+    ("ax2Injectivity", ax2Injectivity),
+    ("ax3neutral", ax3neutral),
+    ("ax4plusSuccessor", ax4plusSuccessor),
+    ("ax5timesZero", ax5timesZero),
+    ("ax6timesDistrib", ax6timesDistrib),
+    ("ax7induction", ax7induction)
+  )
+  peanoAxioms.foreach(a => runningPeanoTheory.addAxiom(a._1, a._2))
+}