proposition: Lemma probadd_neq0 p q : Prob.p p + Prob.p q != 0 <-> p != 0%:pr \/ q != 0%:pr.
proof: Proof. apply/iff_not2; split=> [/negP/negPn/eqP/probadd_eq0[-> ->]|]. by apply/not_orP; split; apply/negP/negPn. move=> /not_orP[/negP/negPn/eqP -> /negP/negPn/eqP -> /=]; apply/negP/negPn. by rewrite addr0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)