proposition: Lemma Cauchy_IR_le_as_CR_le : forall (x y:Cauchy_IR), (Cauchy_IRasCR x <= Cauchy_IRasCR y)%CR <-> x[<=]y.
proof: Proof. intros [x Hx] [y Hy]. split. intros H1 [n [e He H2]]. assert (H1':=H1 ((1#3)*(exist _ _ He))%Qpos). clear H1. simpl in H1'. unfold Cap_raw in H1'; simpl in H1'. destruct (Hy (proj1_sig ((1 # 2) * ((1#3)* exist _ _ He))%Qpos)) as [n1 Hn1] in H1'. destruct (Hx (proj1_sig ((1 # 2) * ((1#3)* exist _ _ He))%Qpos)) as [n2 Hn2] in H1'. simpl in H2. set (m:=Nat.max n (Nat.max n1 n2)). assert (m1:n<=m);[unfold m; auto with *|]. assert (m2:n1<=m);[unfold m; apply Nat.le_trans with (Nat.max n1 n2); auto with *|]. assert (m3:n2<=m);[unfold m; apply Nat.le_trans with (Nat.max n1 n2); auto with *|]. apply (Qle_not_lt _ _ H1'). eapply inv_cancel_less;simpl. clear H1'. autorewrite with QposElim in *. apply Qlt_le_trans with ((2#3)*e)%Q. ring_simplify. eapply mult_resp_less. constructor. assumption. stepl (e + - ((1#2)*((1#3)*e)) + - ((1#2)*((1#3)*e)))%Q; [| simpl; ring]. stepr ((x m - y m) + (y m - y n1) + -(x m - x n2))%Q; [| simpl; ring]. eapply plus_resp_leEq_both. apply plus_resp_leEq_both. apply H2; assumption. refine (proj1 (Hn1 m _));assumption. apply inv_resp_leEq. refine (proj2 (Hn2 m _));assumption. intros H e. simpl. unfold Cap_raw; simpl. destruct (Hy (proj1_sig ((1 # 2) * e)%Qpos)) as [n1 Hn1]. destruct (Hx (proj1_sig ((1 # 2) * e)%Qpos)) as [n2 Hn2]. apply Qnot_lt_le. intros A. apply H; clear H. exists (Nat.max n1 n2). simpl. set (n:=Nat.max n1 n2). exists (- proj1_sig e + - (y n1 + - x n2))%Q. rewrite <- Qlt_minus_iff. assumption. intros m Hm. unfold cg_minus. simpl. stepr ((x m - x n2) + -(y m - y n1) + -(y n1 + - x n2))%Q; [| simpl; ring]. eapply plus_resp_leEq. stepl (-((1 # 2) * proj1_sig e) + - ((1 # 2) * proj1_sig e))%Q; [| simpl; ring]. apply plus_resp_leEq_both. refine (proj1 (Hn2 _ _)). apply Nat.le_trans with n; [unfold n;auto with *|assumption]. apply inv_resp_leEq. refine (proj2 (Hn1 _ _)). apply Nat.le_trans with n; [unfold n;auto with *|assumption]. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps