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