proposition: Lemma dinsupp_restr (mu : {distr T / R}) (p : pred T) x : (x \in dinsupp (drestr p mu)) = (x \in dinsupp mu) && p x.
proof: Proof. apply/dinsuppP/idP. - by rewrite drestrE; case: ifP=> // _ /dinsuppP ->. - by case/andP; rewrite drestrE => /dinsuppP ? ->. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum