fact: Fixpoint rnds (s : RandomSeed) (n' : nat) : list RandomSeed := match n' with | O => nil | S n'' => let (s1, s2) := randomSplit s in cons s1 (rnds s2 n'') end.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)