proposition: Lemma prob_gt0 p : p != 0%:pr <-> 0 < Prob.p p.
proof: Proof. rewrite lt_neqAle; split=> [H|/andP[+ pge0]]. by apply/andP; split; [rewrite eq_sym|exact: prob_ge0]. by apply: contra => /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)