proposition: Lemma Rlt_ge_dec : forall r1 r2, {r1 < r2} + {r1 >= r2}.
proof: Proof. intros. destruct (total_order_T r1 r2). destruct s. exact (left r). exact (right (Req_ge r1 r2 e)). exact (right (Rle_ge r2 r1 (Rlt_le r2 r1 r))). Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations