proposition: Lemma support_sub_diag_mgs { A : choiceType } ( d : SDistr (prod_choiceType A A) ) (Hsupp : forall a1 a2, 0 < d (a1, a2) -> a1 = a2) : forall a : A, lmg d a = d (a, a) /\ rmg d a = d (a, a).
proof: Proof. move => a. rewrite /lmg /rmg dfstE dsndE. split. - rewrite psum_sum. rewrite (sum_seq1 a). + reflexivity. + move => y Hdd. specialize (Hsupp a y). assert (0 < d (a, y)) as Hd. { rewrite lt_def. apply /andP. split. - assumption. - apply (ge0_mu d). } specialize (Hsupp Hd). rewrite Hsupp. auto. + move => x. apply (ge0_mu d). - rewrite psum_sum. rewrite (sum_seq1 a). + reflexivity. + move => y Hdd. specialize (Hsupp y a). assert (0 < d (y, a)) as Hd. { rewrite lt_def. apply /andP. split. - assumption. - apply (ge0_mu d). } specialize (Hsupp Hd). rewrite Hsupp. auto. + move => x. apply (ge0_mu d). Qed.
imports: Coq(Relation_Definitions 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)