proposition: Theorem coarbComplete : forall {A : Type} `{_ : CoArbitrary A} (max : A) (f : A -> RandomSeed), exists seed, forall a, coarbLe a max -> varySeed (posToPath (coarbitrary a)) seed = f a.
proof: Proof. intros. pose proof (coarbComplete' (coarbitrary max) (funToPosFun f)) as Hyp. inversion Hyp as [seed HSeed]; clear Hyp. exists seed. intros a HLe. pose proof (HSeed (coarbitrary a)) as HCo; clear HSeed. apply coarbLePreservesLe in HLe. apply HCo in HLe; clear HCo. rewrite HLe; clear HLe. unfold funToPosFun. rewrite coarbCorrect. reflexivity. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets