proposition: Lemma d_inv_coupling {A1 A2} {c1 : SDistr A1} {c2 : SDistr A2} (d : SDistr (F_choice_prod ⟨ A1, A2 ⟩ )) (d_coupling : coupling d c1 c2) : coupling (d_inv d) c2 c1.
proof: Proof. unfold coupling. split. - unfold lmg. unfold d_inv. apply distr_ext. move=> x. erewrite (dfst_dswap d). destruct d_coupling as [lH rH]. rewrite -rH. unfold rmg. reflexivity. - unfold rmg. unfold d_inv. apply distr_ext. move=> x. erewrite (dsnd_dswap d). destruct d_coupling as [lH rH]. rewrite -lH. unfold lmg. reflexivity. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum finmap.set finmap.finmap xfinmap) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type)