proposition: Lemma probmul_eq1 p q : Prob.p p * Prob.p q = 1 <-> p = 1%:pr /\ q = 1%:pr.
proof: Proof. split => [/= pq1|[-> ->]]; last by rewrite mulr1. move: (oner_neq0 R); rewrite -{1}pq1 mulf_eq0 negb_or => /andP[p0 q0]. have := prob_le1 p; rewrite le_eqVlt => /orP[/eqP p1|p1]. by rewrite p1 mul1r in pq1; split; exact/val_inj. have := prob_le1 q; rewrite le_eqVlt => /orP[/eqP q1|q1]. by rewrite q1 mulr1 in pq1; split; exact/val_inj. have {}p0 : 0 < Prob.p p by rewrite lt_neqAle prob_ge0 eq_sym andbT. by move: p1; rewrite -[in X in X -> _]pq1 (ltr_pMr _ p0) ltNge (ltW q1). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)