proposition: Lemma prob_invp_subproof (p : {prob R}) : (0 <= 1 / (1 + Prob.p p) <= 1)%O.
proof: Proof. apply/andP; split. by rewrite RdivE' mul1r invr_ge0 ?addr_ge0. rewrite RdivE' mul1r invf_le1//. by rewrite ler_addl. rewrite (@lt_le_trans _ _ 1)//. by rewrite ltr01. by rewrite ler_addl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)