proposition: Lemma splitExpand st : exists s, SubSeedTree st (mkSeedTree s).
proof: Proof. elim: st => [|r|st1 [s1 st_s1] st2 [s2 st_s2]]. + by case: randomSeed_inhabited=> seed; exists seed; apply: SubUndef. + by exists r; rewrite mkSeedTreeHelper; constructor. + have [s eq_s] := randomSplitAssumption s1 s2. by exists s; rewrite mkSeedTreeHelper eq_s; constructor. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List