proposition: Lemma Rbar_lt_le_dec (x y : Rbar) : {Rbar_lt x y} + {Rbar_le y x}.
proof: Proof. destruct (Rbar_total_order x y) as [[H|H]|H]. now left. right. rewrite H. apply Rbar_le_refl. right. now apply Rbar_lt_le. Qed.
imports: Coq(Reals ssreflect) Rcomplements