diff --git a/testcases/proof/proba/Coins.scala b/testcases/proof/proba/Coins.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc18f650ec4bd7257e8485b5674a2f9a48349a64
--- /dev/null
+++ b/testcases/proof/proba/Coins.scala
@@ -0,0 +1,71 @@
+import leon.annotation._
+import leon.lang._
+
+object Coins {
+
+  /*
+   * number of outcomes for each face
+   */
+  case class CoinDist(pHead: BigInt, pTail: BigInt)
+
+
+  def isUniform(dist: CoinDist): Boolean = {
+    require(isDist(dist))
+    dist.pHead == dist.pTail
+  }
+
+  def isDist(dist: CoinDist): Boolean = 
+    dist.pHead >= 0 && dist.pTail >= 0 && (dist.pHead > 0 || dist.pTail > 0)
+
+  //sum modulo: face is 0, tail is 1
+  def sum(coin1: CoinDist, coin2: CoinDist): CoinDist = {
+    require(isDist(coin1) && isDist(coin2))
+    CoinDist(
+      coin1.pHead*coin2.pHead + coin1.pTail*coin2.pTail,
+      coin1.pHead*coin2.pTail + coin1.pTail*coin2.pHead
+    )
+  }
+
+  def sumIsUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isUniform(coin1) && isUniform(coin2))
+    val dist = sum(coin1, coin2)
+    isUniform(dist)
+  } holds
+
+  def sumIsUniform2(coin1: CoinDist, coin2: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isUniform(coin1))
+    val dist = sum(coin1, coin2)
+    isUniform(dist)
+  } holds
+
+  //sum of two non-uniform dices is potentially uniform (no result)
+  def sumNonUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && !isUniform(coin1) && !isUniform(coin2))
+    val dist = sum(coin1, coin2)
+    !isUniform(dist)
+  } holds
+
+  def sumNonUniform2(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isDist(coin3) && !isUniform(coin1) && !isUniform(coin2) && !isUniform(coin3))
+    val dist = sum(sum(coin1, coin2), coin3)
+    !isUniform(dist)
+  } //holds
+
+
+  def sumUniform3(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isDist(coin3) && isUniform(coin1))
+    val dist = sum(sum(coin1, coin2), coin3)
+    isUniform(dist)
+  } holds
+
+  def sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2))
+    sum(coin1, coin2) == sum(coin2, coin1)
+  } holds
+
+  def sumIsAssociative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+    require(isDist(coin1) && isDist(coin2) && isDist(coin3))
+    sum(sum(coin1, coin2), coin3) == sum(coin1, sum(coin2, coin3))
+  } holds
+
+}
diff --git a/testcases/proof/proba/Dices.scala b/testcases/proof/proba/Dices.scala
index 0dcd2f1e64e176d7e2f8ebfc9b3455a9f602f306..d7ac55f5645f0e6ad23343d1a0186679f349c515 100644
--- a/testcases/proof/proba/Dices.scala
+++ b/testcases/proof/proba/Dices.scala
@@ -84,4 +84,11 @@ object Dices {
     isUniform(dist)
   } holds
 
+  //sum of two non-uniform dices is potentially uniform (no result)
+  def sumModNonUniform(dice1: DiceDist, dice2: DiceDist): Boolean = {
+    require(isDist(dice1) && isDist(dice2) && !isUniform(dice1) && !isUniform(dice2))
+    val dist = sumMod(dice1, dice2)
+    !isUniform(dist)
+  } holds
+
 }