proposition: Lemma Rbar_total_order (x y : Rbar) : {Rbar_lt x y} + {x = y} + {Rbar_lt y x}.
proof: Proof. destruct x ; destruct y ; simpl ; intuition. destruct (total_order_T r r0) ; intuition. Qed.
imports: Coq(Reals ssreflect) Rcomplements