Library discprob.basic.order

Require Export RelationClasses Morphisms.
From discprob.basic Require Import base.
From mathcomp Require Import ssreflect ssrbool eqtype.
From Coquelicot Require Import Hierarchy.

Require Import Reals.
Instance Rge_Transitive: Transitive Rge.
Instance Rle_Transitive: Transitive Rle.
Instance Rge_Reflexive: Reflexive Rge.
Instance Rle_Reflexive: Reflexive Rle.
Instance Rgt_Transitive: Transitive Rgt.
Instance Rlt_Transitive: Transitive Rlt.

Import Rbar.
Instance Rbar_le_Transitive: Transitive Rbar_le.
Instance Rbar_le_Reflexive: Reflexive Rbar_le.
Instance Rbar_lt_Transitive: Transitive Rbar_lt.

Instance ge_Transitive: Transitive ge.
Instance le_Transitive: Transitive le.
Instance ge_Reflexive: Reflexive ge.
Instance le_Reflexive: Reflexive le.
Instance gt_Transitive: Transitive gt.
Instance lt_Transitive: Transitive lt.


Definition R_eqP : Equality.axiom (fun x y: R ⇒ Req_EM_T x y).

Canonical R_eqMixin := EqMixin R_eqP.
Canonical R_eqType := Eval hnf in EqType R R_eqMixin.

Require Import Psatz.
Instance Rlt_plus_proper: Proper (Rlt ==> Rlt ==> Rlt) Rplus.
Instance Rlt_plus_proper': Proper (Rlt ==> eq ==> Rlt) Rplus.
Instance Rlt_plus_proper'': Proper (Rlt ==> Rle ==> Rlt) Rplus.

Instance Rle_plus_proper_left: Proper (Rle ==> eq ==> Rle) Rplus.
Instance Rle_plus_proper_right: Proper (eq ==> Rle ==> Rle) Rplus.
Instance Rle_plus_proper: Proper (Rle ==> Rle ==> Rle) Rplus.

Lemma Rmax_INR a b: Rmax (INR a) (INR b) = INR (max a b).