proposition: Lemma d_is_one (hCoupl : coupling d (SDistr_unit A1 a1) (SDistr_unit A2 a2)) : d(a1,a2) = 1.
proof: Proof. unshelve epose (@psum_finseq R (F_choice_prod (npair A1 A2)) d [::(a1,a2)] _ _). rewrite cons_uniq //=. move=> [x1 x2]. unfold in_mem. simpl. intro Hsupp. apply /orP. left. move: Hsupp. apply contraLR. intro Hxadiff. unfold "==". simpl. rewrite Bool.negb_involutive. rewrite -/(_ == _). apply /eqP. unshelve eapply lmg_rmg_SDistr_unit. assumption. move: Hxadiff => /negP Hxadiff. intro bla. rewrite bla in Hxadiff. apply Hxadiff. apply eq_refl. move: e. rewrite big_seq1. move=> e. rewrite weight_from_mgs in e. rewrite e. symmetry. assert (Hbnorm: `|d (a1, a2)| == d (a1, a2) -> `|d (a1, a2)| = d (a1, a2)). move=> /eqP. trivial. apply Hbnorm. rewrite -(ger0_def). destruct d as [d1 d2 d3 d4]. simpl in *. apply (d2 (a1,a2)). 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)