diff --git a/testcases/proof/proba/Dices.scala b/testcases/proof/proba/Dices.scala
index 148e6d57895adc2f326d7d8e918c69a977d0ba62..0dcd2f1e64e176d7e2f8ebfc9b3455a9f602f306 100644
--- a/testcases/proof/proba/Dices.scala
+++ b/testcases/proof/proba/Dices.scala
@@ -4,7 +4,7 @@ import leon.lang._
 object Dices {
 
   /*
-   * number of outcomes for each number of a dice
+   * number of outcomes for each face of a dice
    */
   case class DiceDist(p1: BigInt, p2: BigInt, p3: BigInt, p4: BigInt, p5: BigInt, p6: BigInt)
 
@@ -38,6 +38,7 @@ object Dices {
     )
   }
 
+  //distribution of the addition modulo 6 of two dices
   def sumMod(dice1: DiceDist, dice2: DiceDist): DiceDist = {
     require(isDist(dice1) && isDist(dice2))
     DiceDist(
@@ -46,7 +47,7 @@ object Dices {
       dice1.p1*dice2.p2 + dice1.p2*dice2.p1 + dice1.p3*dice2.p6 + dice1.p4*dice2.p5 + dice1.p5*dice2.p4 + dice1.p6*dice2.p3, //3
       dice1.p1*dice2.p3 + dice1.p2*dice2.p2 + dice1.p3*dice2.p1 + dice1.p4*dice2.p6 + dice1.p5*dice2.p5 + dice1.p6*dice2.p4, //4
       dice1.p1*dice2.p4 + dice1.p2*dice2.p3 + dice1.p3*dice2.p2 + dice1.p4*dice2.p1 + dice1.p5*dice2.p6 + dice1.p6*dice2.p5, //5
-      dice1.p1*dice2.p5 + dice1.p2*dice2.p4 + dice1.p3*dice2.p3 + dice1.p4*dice2.p2 + dice1.p5*dice2.p1 + dice1.p6*dice2.p6 //6
+      dice1.p1*dice2.p5 + dice1.p2*dice2.p4 + dice1.p3*dice2.p3 + dice1.p4*dice2.p2 + dice1.p5*dice2.p1 + dice1.p6*dice2.p6  //6
     )
   }
 
@@ -65,10 +66,10 @@ object Dices {
     require(isDist(dice1) && isDist(dice2) && isUniform(dice1) && isUniform(dice2))
     val dist = sum(dice1, dice2)
     
-    dist.p7 >  dist.p1  && dist.p7 >  dist.p2  && dist.p7 >  dist.p3  &&
-    dist.p7 >  dist.p4  && dist.p7 >  dist.p5  && dist.p7 >  dist.p6  &&
-    dist.p7 >= dist.p7  && dist.p7 >  dist.p8  && dist.p7 >  dist.p9  &&
-    dist.p7 >  dist.p10 && dist.p7 >  dist.p11 && dist.p7 >  dist.p12
+    dist.p7 >  dist.p1  && dist.p7 > dist.p2  && dist.p7 > dist.p3  &&
+    dist.p7 >  dist.p4  && dist.p7 > dist.p5  && dist.p7 > dist.p6  &&
+    dist.p7 >= dist.p7  && dist.p7 > dist.p8  && dist.p7 > dist.p9  &&
+    dist.p7 >  dist.p10 && dist.p7 > dist.p11 && dist.p7 > dist.p12
   } holds
 
   def sumModIsUniform1(dice1: DiceDist, dice2: DiceDist): Boolean = {
@@ -82,4 +83,5 @@ object Dices {
     val dist = sumMod(dice1, dice2)
     isUniform(dist)
   } holds
+
 }
diff --git a/testcases/proof/proba/FiniteDistributions.scala b/testcases/proof/proba/FiniteDistributions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81b4ea581135304708acfd4105e08dd431760be0
--- /dev/null
+++ b/testcases/proof/proba/FiniteDistributions.scala
@@ -0,0 +1,79 @@
+import leon.annotation._
+import leon.lang._
+import leon.collection._
+
+object FiniteDistributions {
+
+  /*
+   * number of outcomes for each index (ps(0) outcomes of value 0, ps(1) outcomes of value 1).
+   * Sort of generalization of a dice distribution
+   */
+  //case class FiniteDist(ps: List[BigInt])
+
+  case class FiniteDist(domain: List[BigInt], outcomes: Map[BigInt, BigInt])
+
+  def isUniform(dist: FiniteDist): Boolean = dist.domain match {
+    case Nil() => true
+    case Cons(x, Nil()) => true
+    case Cons(x, rest@Cons(y, _)) => outcomes(x) == outcomes(y) && isUniform(FiniteDist(rest, dist.domain))
+  }
+
+  def isDist(dist: FiniteDist): Boolean = {
+    
+    def allPos(dist: FiniteDist): Boolean = dist.ps match {
+      case Cons(x, Nil()) => x >= 0
+      case Cons(x, xs) => x >= 0 && isDist(xs)
+    }
+    def atLeastOne(dist: FiniteDist): Boolean = dist.ps match {
+      case Cons(x, xs) => x > 0 || atLeastOne(xs)
+      case Nil => false
+    }
+
+    allPos(dist) && atLeastOne(dist)
+  }
+
+  def probaHead(dist1: FiniteDist, dist2: FiniteDist): BigInt = {
+    require(isDist(dist1) && isDist(dist2) && dist1.size == dist2.size)
+    if(dist1.ps.isEmpty) 0 else dist1.head*dist2.last + probaHead(dist1.tail, dist2.init)
+  }
+
+  def sumMod(dist1: FiniteDist, dist2: FiniteDist): FiniteDist = {
+    require(isDist(dist1) && isDist(dist2) && dist1.size == dist2.size)
+
+    def 
+    rotate(1)
+  }
+
+  def uniformSumProperties1(dice1: DiceDist, dice2: DiceDist): Boolean = {
+    require(isDist(dice1) && isDist(dice2) && isUniform(dice1) && isUniform(dice2))
+    val dist = sum(dice1, dice2)
+
+    dist.p2 == dist.p12 &&
+    dist.p3 == dist.p11 &&
+    dist.p4 == dist.p10 &&
+    dist.p5 == dist.p9 &&
+    dist.p6 == dist.p8
+  } holds
+  
+  def uniformSumMostLikelyOutcome(dice1: DiceDist, dice2: DiceDist): Boolean = {
+    require(isDist(dice1) && isDist(dice2) && isUniform(dice1) && isUniform(dice2))
+    val dist = sum(dice1, dice2)
+    
+    dist.p7 >  dist.p1  && dist.p7 > dist.p2  && dist.p7 > dist.p3  &&
+    dist.p7 >  dist.p4  && dist.p7 > dist.p5  && dist.p7 > dist.p6  &&
+    dist.p7 >= dist.p7  && dist.p7 > dist.p8  && dist.p7 > dist.p9  &&
+    dist.p7 >  dist.p10 && dist.p7 > dist.p11 && dist.p7 > dist.p12
+  } holds
+
+  def sumModIsUniform1(dice1: DiceDist, dice2: DiceDist): Boolean = {
+    require(isDist(dice1) && isDist(dice2) && isUniform(dice1) && isUniform(dice2))
+    val dist = sumMod(dice1, dice2)
+    isUniform(dist)
+  } holds
+
+  def sumModIsUniform2(dice1: DiceDist, dice2: DiceDist): Boolean = {
+    require(isDist(dice1) && isDist(dice2) && isUniform(dice1))
+    val dist = sumMod(dice1, dice2)
+    isUniform(dist)
+  } holds
+}
diff --git a/testcases/proof/proba/RandomVariables.scala b/testcases/proof/proba/RandomVariables.scala
new file mode 100644
index 0000000000000000000000000000000000000000..74899bb46648bd3141ec2cd33c99edc19c389247
--- /dev/null
+++ b/testcases/proof/proba/RandomVariables.scala
@@ -0,0 +1,8 @@
+import leon.annotation._
+import leon.lang._
+
+object RandomVariables {
+
+  //case class RandomVariable(p: (BigInt) => Real, 
+}
+