proposition: Lemma oprobadd_neq0 p q : Prob.p (OProb.p p) + Prob.p (OProb.p q) != 0%coqR.
proof: Proof. by move: (oprobadd_gt0 p q); rewrite ltR_neqAle => -[] /nesym /eqP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)