proposition: Lemma le1_prc A B mu : \P_[mu, B] A <= 1.
proof: Proof. have := ge0_pr B mu; rewrite /prc le_eqVlt. case/orP=> [/eqP<-|]; first by rewrite invr0 mulr0 ler01. by move/ler_pdivrMr=> ->; rewrite mul1r le_in_pr // => x _ /andP[]. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum