diff --git a/prelude/nat.lp b/prelude/nat.lp
new file mode 100644
index 0000000000000000000000000000000000000000..0306c9d655b0e62910c27315bfe830cc69cddca5
--- /dev/null
+++ b/prelude/nat.lp
@@ -0,0 +1,9 @@
+require open pvs_core prelude.notequal
+// Not part of prelude as integers are built in pvs
+
+constant symbol int : Type
+symbol zero : eta int
+symbol succ (_: eta int) : eta int
+
+set builtin "0" ≔ zero
+set builtin "+1" ≔ succ
diff --git a/prelude/nat_ops.lp b/prelude/nat_ops.lp
new file mode 100644
index 0000000000000000000000000000000000000000..4d5687c66f7bdb541c0b152268767691dd77cb82
--- /dev/null
+++ b/prelude/nat_ops.lp
@@ -0,0 +1,7 @@
+require open pvs_core prelude.notequal prelude.nat
+symbol times : eta int ⇒ eta int ⇒ eta int
+rule times &n 1 → &n
+
+// x =/= 0 ∧ y =/= 0 ⇒ x * y =/= 0
+symbol prod_not_zero (x y: eta int) :
+  eps (neq int x 0) ⇒ eps (neq int y 0) ⇒ eps (neq int (times x y) 0)
diff --git a/prelude/rat1.lp b/prelude/rat1.lp
new file mode 100644
index 0000000000000000000000000000000000000000..fcb2355ebb0bba1d8ab9abaeb290b7ac51501d45
--- /dev/null
+++ b/prelude/rat1.lp
@@ -0,0 +1,26 @@
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
+prelude.nat
+require prelude.nat_ops as N
+
+constant symbol rat : Type
+constant symbol zero : eta rat
+
+symbol frac (n : eta int) (m : eta int) (pi : eps (neq int m 0)) : eta rat
+
+symbol div : eta rat ⇒ eta rat ⇒ eta rat
+symbol times : eta rat ⇒ eta rat ⇒ eta rat
+set infix 5 "*" ≔ times
+set infix 6 "/" ≔ div
+
+rule times (frac &A &B &X) (frac &C &D &Y) →
+  frac (N.times &A &C) (N.times &B &D) (N.prod_not_zero &B &D &X &Y)
+
+symbol rateq : eta rat ⇒ eta rat ⇒ eta Prop
+rule rateq (frac &A &B &Pi) (frac &C &D &Pi') →
+  eq int (N.times &A &D) (N.times &B &C)
+
+theorem t1 : ∀ a b : eta int, ∀ pi : eps (neq int b 0), ∀ pi' : eps (neq int 1 0),
+  eps (rateq ((frac a b pi) * (frac b 1 pi')) (frac a 1 pi'))
+proof
+assume a b pi pi'
+admit