proposition: Lemma lmg_rmg_SDistr_unit (hCoupl : coupling d (SDistr_unit A1 a1) (SDistr_unit A2 a2)) : forall (x1 : A1) (x2 : A2), ~( (x1,x2) = (a1,a2) ) -> d(x1,x2) = 0.
proof: Proof. intros. move: hCoupl => [lH rH]. case HXA : (x1 != a1). - eapply lmg_SDistr_unit. assumption. unshelve eapply elimT in HXA. exact (~(x1 = a1)). intro. symmetry in H0. apply HXA. assumption. eapply Bool.iff_reflect. split. intro. assumption. intros. intro. rewrite H1 in HXA. move: HXA => /negP HXA. apply HXA. apply /eqP. reflexivity. - unshelve eapply introN in H. exact ((x1,x2)==(a1,a2)). all: revgoals. apply eqP. simpl in H. unfold "==" in H. simpl in H. rewrite Bool.negb_andb in H. rewrite HXA in H. simpl in H. eapply rmg_SDistr_unit. assumption. move: H => /negP H. intro Ha2x2. rewrite Ha2x2 in H. apply H. apply /eqP. reflexivity. 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)