proposition: Lemma ge_s_of p q : (Prob.p p <= Prob.p [s_of p, q])%mcR.
proof: Proof. rewrite s_of_pqE. rewrite onemE. rewrite addrC. rewrite -lerBlDr. rewrite -opprB. rewrite lerNl opprK. rewrite -/(Prob.p p).~. rewrite ler_piMr//. by apply: onem_le1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)