proposition: Lemma Rle_ge_dec : forall r1 r2, {r1 <= r2} + {~ r2 >= r1}.
proof: Proof. intros. destruct (total_order_T r1 r2). destruct s. apply (left (Rlt_le r1 r2 r)). apply (left (Req_le r1 r2 e)). apply (right (Rlt_not_ge r2 r1 r)). Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations