object Fractions { // fraction is a pair fr: (BigInt,BigInt) where fr._2 > 0.   
    // (numerator,denominator) representing numerator/denominator
    def good(fr: (BigInt, BigInt)): Boolean = fr._2 > 0

    def mul(fr1: (BigInt,BigInt), fr2: (BigInt, BigInt)): (BigInt, BigInt) = {
      require(good(fr1) && good(fr2))
      (fr1._1 * fr2._1, fr1._2 * fr2._2)
    } ensuring (res => good(res))

    def com(fr1: (BigInt,BigInt), fr2: (BigInt, BigInt)): Unit = {
     require(good(fr1) && good(fr2))
    }.ensuring(_ => mul(fr1, fr2)==mul(fr2,fr1))

    def assoc(fr1: (BigInt,BigInt), 
              fr2: (BigInt, BigInt),
              fr3: (BigInt, BigInt)): Unit = {
      require(good(fr1) && good(fr2) && good(fr3))

      val LHS: (BigInt,BigInt) = mul(mul(fr1, fr2), fr3)
      assert(LHS._1 == (fr1._1 * fr2._1) * fr3._1)
      assert(LHS._2 == (fr1._2 * fr2._2) * fr3._2)

    }.ensuring(_ => mul(mul(fr1, fr2), fr3)==mul(fr1, mul(fr2, fr3)))
}
