proposition: Lemma paddR_neq0 (p q : R) (p0 : 0 <= p) (q0 : 0 <= q) : p + q != 0 <-> p != 0 \/ q != 0.
proof: Proof. split => [H | /orP]. - apply/orP; rewrite -negb_and; apply: contra H => /andP[/eqP -> /eqP ->]. by rewrite addR0. - rewrite -negb_and; apply: contra => /eqP/paddR_eq0. by case/(_ p0)/(_ q0) => -> ->; rewrite eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)