proposition: Lemma Rbar_opp_lt (x y : Rbar) : Rbar_lt (Rbar_opp x) (Rbar_opp y) <-> Rbar_lt y x.
proof: Proof. destruct x as [x | | ] ; destruct y as [y | | ] ; split ; auto ; intro H ; simpl ; try left. apply Ropp_lt_cancel ; auto. apply Ropp_lt_contravar ; auto. Qed.
imports: Coq(Reals ssreflect) Rcomplements