proposition: Lemma mkSeedTreeHelper r : mkSeedTree r = RstNode r (mkSeedTree (randomSplit r).1) (mkSeedTree (randomSplit r).2).
proof: Proof. by rewrite [mkSeedTree _]rst_eta /=; case: (randomSplit r). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics