proposition: Lemma p_of_rs1 r s : ([p_of r, s] == 1%:pr :> {prob R}) = ((r == 1%:pr) && (s == 1%:pr)).
proof: Proof. apply/idP/idP; last by case/andP => /eqP -> /eqP ->; rewrite p_of_r1. move/eqP/(congr1 (@Prob.p _)). rewrite /= p_of_rsE => /eqP. apply contraLR => /nandP. wlog : r s / r != 1%:pr by move=> H [|] ?; [|rewrite mulrC]; rewrite H //; left. move=> r1 _. have [/eqP->|] := boolP (r == 0%:pr :> {prob R}). by rewrite mul0r eq_sym oner_eq0. move/prob_gt0. rewrite lt_neqAle => /andP[r0 _]. apply/eqP. move/(congr1 (fun x => ((Prob.p r)^-1)%mcR * x))%R. rewrite mulrA mulVr ?unitfE//; last by rewrite eq_sym. rewrite mul1r mulr1. rewrite eq_sym in r0. move/prob_gt0 in r0. move=> srV; move: (prob_le1 s); rewrite {}srV. rewrite invr_le1// ?unitfE ?gt_eqF//. apply/negP. rewrite -ltNge. by rewrite -prob_lt1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)