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