proposition: Lemma p_of_rs_subproof {R : realType} (r s : {prob R}) : (0 <= Prob.p r * Prob.p s <= 1)%R.
proof: Proof. by apply/andP; split; [rewrite mulr_ge0|rewrite mulr_ile1]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)