diff --git a/library/lang/Rational.scala b/library/lang/Rational.scala
index 2d609980d822297a45415e52992e186ec77dc2e4..3be89a7632a42b6b17d069435bf15ce00bea8912 100644
--- a/library/lang/Rational.scala
+++ b/library/lang/Rational.scala
@@ -17,16 +17,26 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
     Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.denominator)
   }
 
+  def unary_- : Rational = {
+    require(this.isRational)
+    Rational(-this.numerator, this.denominator)
+  }
+
   def *(that: Rational): Rational = {
     require(this.isRational && that.isRational)
     Rational(this.numerator*that.numerator, this.denominator*that.denominator)
   }
 
   def /(that: Rational): Rational = {
-    require(this.isRational && that.isRational)
+    require(this.isRational && that.isRational && that.nonZero)
     Rational(this.numerator*that.denominator, this.denominator*that.numerator)
   }
 
+  def reciprocal: Rational = {
+    require(this.isRational && this.nonZero)
+    Rational(this.denominator, this.numerator)
+  }
+
 
   def ~(that: Rational): Boolean = {
     require(this.isRational && that.isRational)
diff --git a/testcases/verification/math/RationalProps.scala b/testcases/verification/math/RationalProps.scala
index ed42a2318f44bb9e14513824cba136e6715d255d..e84b92361f1ca79a7ae23d9b149d6cbeeb48620b 100644
--- a/testcases/verification/math/RationalProps.scala
+++ b/testcases/verification/math/RationalProps.scala
@@ -44,4 +44,24 @@ object RationalProps {
     (p*(q + r)) ~ (p*q + p*r)
   } holds
 
+  def reciprocalIsCorrect(p: Rational): Boolean = {
+    require(p.isRational && p.nonZero)
+    (p * p.reciprocal) ~ Rational(1)
+  } holds
+
+  def additiveInverseIsCorrect(p: Rational): Boolean = {
+    require(p.isRational)
+    (p + (-p)) ~ Rational(0)
+  } holds
+
+  //should not hold because q could be 0
+  def divByZero(p: Rational, q: Rational): Boolean = {
+    require(p.isRational && q.isRational)
+    ((p / q) * q) ~ p
+  } holds
+
+  def divByNonZero(p: Rational, q: Rational): Boolean = {
+    require(p.isRational && q.isRational && q.nonZero)
+    ((p / q) * q) ~ p
+  } holds
 }