Operations on rational numbers over CR are the same as the operations on rational numbers.
Lemma CReq_Qeq : forall (x y:Q), inject_Q x == inject_Q y <-> (x == y)%Q.

Lemma CRle_Qle : forall (x y:Q), inject_Q x <= inject_Q y <-> (x <= y)%Q.

Lemma CRplus_Qplus : forall (x y:Q), inject_Q x + inject_Q y == inject_Q (x + y)%Q.


Lemma CRopp_Qopp : forall (x:Q), - inject_Q x == inject_Q (- x)%Q.
Lemma CRminus_Qminus : forall (x y:Q), inject_Q x - inject_Q y == inject_Q (x - y)%Q.
Lemma CRmult_Qmult : forall (x y:Q), inject_Q x * inject_Q y == inject_Q (x * y)%Q.
Lemma Qap_CRap : forall (x y:Q), (~(x==y))%Q -> (' x)><(' y).

Lemma CRinv_Qinv : forall (x:Q) x_, CRinv (inject_Q x) x_ == inject_Q (/x).

Ring

CR forms a ring for the ring tactic.
Lemma CR_ring_theory :
 @ring_theory CR (' 0%Q) (' 1%Q) (ucFun2 CRplus) CRmult
 (fun (x y:CR) => (x + - y)) CRopp (@st_eq CR).

Lemma inject_Q_strext : fun_strext inject_Q.

Definition inject_Q_csf := Build_CSetoid_fun _ _ _ inject_Q_strext.

Lemma inject_Q_hom : RingHom Q_as_CRing CRasCRing.

Lemma CR_Q_ring_morphism :
 ring_morph (inject_Q 0%Q) (inject_Q 1%Q) (ucFun2 CRplus) CRmult
 (fun x y => (x + - y)) CRopp (@st_eq CR)
  (0%Q) (1%Q) Qplus Qmult Qminus Qopp Qeq_bool (inject_Q).



Lemma CR_ring_eq_ext : ring_eq_ext (ucFun2 CRplus) CRmult CRopp (@st_eq CR).

Add Ring CR_ring : CR_ring_theory (morphism CR_Q_ring_morphism, setoid (@st_isSetoid (@msp_is_setoid CR)) CR_ring_eq_ext, constants [CRcst], preprocess [CRring_pre]).

Relationship between strict and nonstrict positivity
Lemma CRpos_nonNeg : forall x, CRpos x -> CRnonNeg x.

Lemma CRneg_nonPos : forall x, CRneg x -> CRnonPos x.