proposition: Lemma randomSplitAssumption : forall s1 s2 : RandomSeed, exists s, randomSplit s = (s1,s2).
proof: Proof. move => s1 s2. by exists (Node true s1 s2). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List