proposition: Lemma coupling_SDistr_unit_F_choice_prod : coupling d (SDistr_unit A1 a1) (SDistr_unit A2 a2) -> d = SDistr_unit (F_choice_prod (npair A1 A2)) (a1,a2).
proof: Proof. simpl in *. unfold SDistr_carrier in d. move=> hCoupl. apply distr_ext. move=> [x1 x2]. unfold SDistr_unit. assert (xa_lem : (x1,x2) = (a1,a2) \/ ~((x1,x2) = (a1,a2))). apply eqType_lem. destruct xa_lem as [xa_lem_left | xa_lem_right]. rewrite dunit1E. rewrite xa_lem_left. rewrite refl_true. simpl. unshelve eapply d_is_one. assumption. rewrite dunit1E. assert ((a1, a2) == (x1, x2) = false). apply Bool.negb_true_iff. apply /negP. move=> /eqP hxa. symmetry in hxa. apply xa_lem_right. assumption. rewrite H. simpl. unshelve eapply lmg_rmg_SDistr_unit. assumption. assumption. Qed.
imports: Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Coq(RelationClasses Morphisms) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd only_prob.SubDistr)