proposition: Lemma coarbLePreservesLe : forall {A : Type} `{_ : CoArbitrary A} (x y : A), coarbLe x y -> Pos.le (coarbitrary x) (coarbitrary y).
proof: Proof. by []. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets