fact: Definition posFunToPathFun (f : positive -> RandomSeed) (p : SplitPath) : RandomSeed := match pathToPos p with | Some a => f a | None => newRandomSeed end.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets