proposition: Lemma CRisCOrdField : is_COrdField CRasCField CRltasCCsetoidRelation CRle (default_greater _ CRltasCCsetoidRelation) (default_grEq CRasCField CRle).
proof: Proof. split. split. intros x y z H0 H1. apply CR_lt_as_Cauchy_IR_lt_2. apply less_transitive_unfolded with (CRasCauchy_IR y); apply CR_lt_as_Cauchy_IR_lt_1; assumption. intros x y H0 H1. apply (less_antisymmetric_unfolded _ (CRasCauchy_IR x) (CRasCauchy_IR y)); apply CR_lt_as_Cauchy_IR_lt_1; assumption. intros x y H z. change (x+z < y + z)%CR. apply CR_lt_as_Cauchy_IR_lt_2. stepl ((CRasCauchy_IR x)[+](CRasCauchy_IR z)); [| now apply CR_plus_as_Cauchy_IR_plus]. stepr ((CRasCauchy_IR y)[+](CRasCauchy_IR z)); [| now apply CR_plus_as_Cauchy_IR_plus]. apply plus_resp_less_rht. apply CR_lt_as_Cauchy_IR_lt_1. assumption. intros x y Hx Hy. change (0 < x*y)%CR. apply CR_lt_as_Cauchy_IR_lt_2. stepr ((CRasCauchy_IR x)[*](CRasCauchy_IR y)); [| now apply CR_mult_as_Cauchy_IR_mult]. eapply less_wdl;[|apply (CR_inject_Q_as_Cauchy_IR_inject_Q 0)]. apply mult_resp_pos;( eapply less_wdl;[|apply eq_symmetric;apply (CR_inject_Q_as_Cauchy_IR_inject_Q 0)]; apply CR_lt_as_Cauchy_IR_lt_1;assumption). intros x y. split. intros H. destruct (ap_imp_less _ _ _ (CR_ap_as_Cauchy_IR_ap_1 _ _ H));[left|right]; apply CR_lt_as_Cauchy_IR_lt_2; assumption. intros [H|H]; apply CR_ap_as_Cauchy_IR_ap_2; [apply less_imp_ap|apply Greater_imp_ap]; apply CR_lt_as_Cauchy_IR_lt_1;assumption. intros x y. rewrite <- CR_le_as_Cauchy_IR_le. split. intros H0 H1. apply H0. apply CR_lt_as_Cauchy_IR_lt_1. assumption. intros H0 H1. apply H0. apply CR_lt_as_Cauchy_IR_lt_2. assumption. intros x y. split; intros; assumption. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRFieldOps CoRN.model.fields.CRfield CoRN.algebra.COrdFields CoRN.reals.fast.CRcorrect CoRN.tactics.CornTac