proposition: Lemma isd_mrestr (mu : {distr T / R}) : isdistr (mrestr mu).
proof: Proof. split=> [x|J]; first by rewrite /mrestr; case: ifP. move=> eqJ; apply/(@le_trans _ _ (\sum_(j <- J) `|mu j|)). + apply/ler_sum=> i _; rewrite /mrestr; case: ifPn=> _. by apply/ler_norm. by apply/normr_ge0. + by apply/(le_trans _ (le1_mu mu))/gerfinseq_psum. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum