proposition: Corollary swap_eq { A : ord_choiceType } (c1 c2 : MFreePr A) : θ0 (c1 ;; c2) = θ0 (c2 ;; c1).
proof: Proof. apply: coupling_eq. exact: (swap_rule c1 c2). auto. 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)