proposition: Lemma Rbar_abs_neg (x : Rbar) : Rbar_le x 0 -> Rbar_abs x = Rbar_opp x.
proof: Proof. case: x => [x | | ] //= Hx. rewrite -Rabs_Ropp. apply f_equal, Rabs_pos_eq. now rewrite -Ropp_0 ; apply Ropp_le_contravar. Qed.
imports: Coq(Reals ssreflect) Rcomplements