proposition: Lemma R_is_OrdField : is_COrdField RField Rless_rel Rle Rgt_rel Rge.
proof: Proof. constructor. constructor. unfold Ctransitive. apply Rlt_trans. unfold CSetoids.antisymmetric. apply Rlt_asym. intros x y xy z. apply Rplus_lt_compat_r. assumption. intros x y x0 y0. apply Rmult_gt_0_compat; assumption. intros x y. constructor. intro xy. elim (total_order_T x y); intro H2. elim H2; clear H2; intro H3. left; assumption. exfalso; apply xy; assumption. right; assumption. intro H; destruct H. apply: Rlt_not_eq; assumption. apply: Rgt_not_eq; assumption. intros x y. simpl in *. unfold Not; split. intros; lra. intro. apply Rnot_lt_le. assumption. auto with *. auto with *. Qed.
imports: CoRN.algebra.CSetoids CoRN.algebra.CSemiGroups CoRN.algebra.CMonoids CoRN.algebra.CGroups CoRN.tactics.CornTac CoRN.algebra.CAbGroups CoRN.algebra.CRings CoRN.algebra.CFields CoRN.algebra.COrdFields CoRN.reals.CReals Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun Coq(Lra)