diff --git a/library/lang/Rational.scala b/library/lang/Rational.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2d609980d822297a45415e52992e186ec77dc2e4
--- /dev/null
+++ b/library/lang/Rational.scala
@@ -0,0 +1,97 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+@library
+case class Rational(numerator: BigInt, denominator: BigInt) {
+
+  def +(that: Rational): Rational = {
+    require(this.isRational && that.isRational)
+    Rational(this.numerator*that.denominator + that.numerator*this.denominator, this.denominator*that.denominator)
+  }
+
+  def -(that: Rational): Rational = {
+    require(this.isRational && that.isRational)
+    Rational(this.numerator*that.denominator - that.numerator*this.denominator, this.denominator*that.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)
+    Rational(this.numerator*that.denominator, this.denominator*that.numerator)
+  }
+
+
+  def ~(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    this.numerator*that.denominator == that.numerator*this.denominator
+  }
+
+  def <(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator < that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator > that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator > that.numerator*this.denominator
+    else
+      this.numerator*that.denominator < that.numerator*this.denominator
+  }
+
+  def <=(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator <= that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator >= that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator >= that.numerator*this.denominator
+    else
+      this.numerator*that.denominator <= that.numerator*this.denominator
+  }
+
+  def >(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator > that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator < that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator < that.numerator*this.denominator
+    else
+      this.numerator*that.denominator > that.numerator*this.denominator
+  }
+
+  def >=(that: Rational): Boolean = {
+    require(this.isRational && that.isRational)
+    if(this.denominator >= 0 && that.denominator >= 0)
+      this.numerator*that.denominator >= that.numerator*this.denominator
+    else if(this.denominator >= 0 && that.denominator < 0)
+      this.numerator*that.denominator <= that.numerator*this.denominator
+    else if(this.denominator < 0 && that.denominator >= 0)
+      this.numerator*that.denominator <= that.numerator*this.denominator
+    else
+      this.numerator*that.denominator >= that.numerator*this.denominator
+  }
+
+  def nonZero: Boolean = {
+    require(this.isRational)
+    numerator != 0
+  }
+
+  def isRational: Boolean = denominator != 0
+}
+
+object Rational {
+
+  implicit def bigIntToRat(n: BigInt): Rational = Rational(n, 1)
+
+  def apply(n: BigInt): Rational = Rational(n, 1)
+}
diff --git a/testcases/verification/math/RationalProps.scala b/testcases/verification/math/RationalProps.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ed42a2318f44bb9e14513824cba136e6715d255d
--- /dev/null
+++ b/testcases/verification/math/RationalProps.scala
@@ -0,0 +1,47 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object RationalProps {
+
+  def squarePos(r: Rational): Rational = {
+    require(r.isRational)
+    r * r
+  } ensuring(_ >= Rational(0))
+
+  def additionIsCommutative(p: Rational, q: Rational): Boolean = {
+    require(p.isRational && q.isRational)
+    p + q == q + p
+  } holds
+
+  def multiplicationIsCommutative(p: Rational, q: Rational): Boolean = {
+    require(p.isRational && q.isRational)
+    p * q == q * p
+  } holds
+
+  def lessThanIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p < q && q < r)
+    p < r
+  } holds
+
+  def lessEqualsIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p <= q && q <= r)
+    p <= r
+  } holds
+
+  def greaterThanIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p > q && q > r)
+    p > r
+  } holds
+
+  def greaterEqualsIsTransitive(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational && p >= q && q >= r)
+    p >= r
+  } holds
+
+  def distributionMult(p: Rational, q: Rational, r: Rational): Boolean = {
+    require(p.isRational && q.isRational && r.isRational)
+    (p*(q + r)) ~ (p*q + p*r)
+  } holds
+
+}