proposition: Lemma Rge_lt_or_eq_dec : forall r1 r2, (r1 >= r2) -> {r2 < r1} + {r1 = r2}.
proof: Proof. intros. destruct (total_order_T r2 r1). - destruct s. + left. exact r. + right. symmetry. exact e. - exfalso. exact (Rlt_not_ge _ _ r H). Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations