proposition: Theorem coarbComplete' : forall (max : positive) (f : positive -> RandomSeed) , exists seed, forall p, p <= max -> varySeed (posToPath p) seed = f p.
proof: Proof. intros. pose proof (SplitPathCompleteness (map posToPath (rangePos max)) (posFunToPathFun f) (rangePosPrefixFree max)). inversion H; clear H. exists x. intros. pose proof H0 (posToPath p). rewrite H1. + unfold posFunToPathFun. rewrite posPathInj. reflexivity. + apply in_map_iff. exists p. split; auto. apply posLtInRange. auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets