coq - Rbar / Rbar_le / コクリコ補題

Question

Coq 8.12.0 リファレンス マニュアルで Coq を学習していますが、次の補題を証明するのに苦労しています。

From Coq Require Import Lia Reals Lra List.

Lemma lemma1 : forall (x y:Rbar), Rbar_le x 0 -> Rbar_le y 0
   -> Rbar_le (Rbar_plus x y) 0.

Proof.
destruct x ; destruct y ; simpl ; intuition.
destruct H.
destruct H0.
unfold Rle.
auto with real.
right.
...

そして、私は証明を終わらせるのに行き詰まります。何か案は ？