proposition: Lemma probadd_eq0 p q : Prob.p p + Prob.p q = 0 <-> p = 0%:pr /\ q = 0%:pr.
proof: Proof. split; last by move=> [-> ->] /=; rewrite addr0. move/eqP; rewrite paddr_eq0; [|exact: prob_ge0|exact: prob_ge0]. by move=> /andP[/eqP ? /eqP ?]; split; exact/val_inj. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)