proposition: Lemma s_of_gt0 p q : p != 0%:pr -> (0 < Prob.p [s_of p, q])%mcR.
proof: Proof. move=> p0; rewrite s_of_pqE; apply: onem_gt0. have [->/=|q0] := eqVneq q 0%:pr. by rewrite onem0 mulr1 onem_lt1// lt0r p0/=. rewrite mulr_ilte1 => //. by rewrite onem_lt1// lt0r p0/=. by rewrite onem_lt1// lt0r q0/=. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)