proposition: Lemma isd_mrat s : isdistr (mrat s).
proof: Proof. by split; [apply/ge0_mrat | apply/has_sup_mrat]. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum