diff --git a/prelude/rat.lp b/prelude/rat.lp
index 9e9666fddf17949760db05fa6f4b6b2f7686f7a4..65a9f0642a0316ab538811c8be7ee44d8381552c 100644
--- a/prelude/rat.lp
+++ b/prelude/rat.lp
@@ -1,18 +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 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
 
-symbol zero_times : ∀ x : eta rat, eps (eq rat zero (zero * x))
+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 nonzero : eta (psub rat (λ x : eta rat, neq rat zero x))
+symbol rateq : eta rat ⇒ eta rat ⇒ eta Prop
+rule rateq (frac &A &B &Pi) (frac &C &D &Pi') →
+  eq (N.times &A &D) (N.times &B &C)
 
-// x * y / x = y
-symbol left_cancellation (x: eta nonzero) (y: eta rat) :
-  eps (eq rat (x * y / x) y)
+theorem t1 : ∀ a b : eta int, ∀ pi : eps (neq b 0), ∀ pi' : eps (neq 1 0),
+  eps (rateq ((frac a b pi) * (frac b 1 pi')) (frac a 1 pi'))
+proof
+assume a b pi pi'
+admit
diff --git a/prelude/rat1.lp b/prelude/rat1.lp
deleted file mode 100644
index 65a9f0642a0316ab538811c8be7ee44d8381552c..0000000000000000000000000000000000000000
--- a/prelude/rat1.lp
+++ /dev/null
@@ -1,26 +0,0 @@
-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 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 (N.times &A &D) (N.times &B &C)
-
-theorem t1 : ∀ a b : eta int, ∀ pi : eps (neq b 0), ∀ pi' : eps (neq 1 0),
-  eps (rateq ((frac a b pi) * (frac b 1 pi')) (frac a 1 pi'))
-proof
-assume a b pi pi'
-admit