fact: Axiom randomRIntCorrect: forall z z1 z2, Z.leb z1 z2 -> (Z.leb z1 z && Z.leb z z2 <-> exists seed, (fst (randomRInt (z1, z2) seed)) = z).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List