proposition: Corollary coupling_le { A : ord_choiceType } (K1 K2 : MFreePr A ) { Ψ : Prop } (H : ⊨ ⦃ Ψ ⦄ K1 ≈ K2 ⦃ eq ⦄): Ψ -> (forall x, (θ0 K1) x <= (θ0 K2) x).
proof: Proof. move => Hpsi a. repeat rewrite pr_pred1. apply: (Pr_le Ψ _ ); rewrite //= => x y Heq. by subst. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod)