Lemma `nadde_lt0` is too restrictive

[hoheinzollern]

Currently in MCA it looks as follows:

Lemma nadde_lt0 (x y : \bar R) :
  x <= 0 -> y <= 0 -> x + y < 0 -> (x < 0) || (y < 0).

we can avoid the two hypotheses:

Lemma nadde_lt0 (x y : \bar R) :
  (x + y < 0 -> (x < 0) || (y < 0)).
Proof.
move: x y => [x| |] [y| |]//; rewrite ?lee_fin ?lte_fin.
- rewrite !ltNge -negb_and; apply: contra.
  by move=> /andP[x0' y0']; rewrite addr_ge0.
- by move=> _; rewrite ltNyr orbT.
- by move=> _; rewrite ltNyr.
- by move=> _; rewrite ltNy0.
- by rewrite ltNy0.
Qed.