proposition: Lemma Cauchy_IR_inv_as_CRinv_pos : forall (x:Cauchy_IR) x_, forall (z:Qpos) (N:nat), (forall i:nat, (N<=i) -> (proj1_sig z <= (CS_seq _ x i))%Q) -> (CRinv_pos z (Cauchy_IRasCR x) == Cauchy_IRasCR (f_rcpcl x (@inr _ _ x_)))%CR.
proof: Proof. intros [x Hx] [a [d d_ x_]] z n Hn. apply regFunEq_equiv, regFunEq_e. intros e. simpl. unfold Qinv_modulus. destruct (Hx (proj1_sig z * proj1_sig z * proj1_sig e)%Q) as [b Hb]. destruct (CS_seq_recip) as [c Hc]. set (y := (CS_seq_recip_seq Q_as_COrdField x d d_ a (fun (n : nat) (H : le a n) => leEq_wdr Q_as_COrdField d (@cg_minus Q_as_CGroup (x n) (Qmake Z0 xH)) (x n) (x_ n H) (cg_inv_zero Q_as_CGroup (x n))))) in *. unfold CS_seq_recip_seq in y. simpl in y. set (m:=Nat.max (Nat.max a n) (Nat.max b c)). assert (Hm1: c<=m). unfold m; apply Nat.le_trans with (Nat.max b c); auto with *. change (@ball Q_as_MetricSpace (proj1_sig e+proj1_sig e) (/ Qmax (proj1_sig z) (x b))%Q (y c)). apply ball_triangle with (y m);[|eapply Hc;assumption]. clear Hc. unfold y. destruct (lt_le_dec m a) as [Z|Z]. elim (proj1 (Nat.le_ngt _ _) Z). unfold m. apply Nat.lt_le_trans with (S (Nat.max a n)); auto with *. change (AbsSmall (proj1_sig e) (/ Qmax (proj1_sig z) (x b)-1 * / x m))%Q. clear y. assert (T:(~ (x m == 0)%Q /\ ~ (Qmax (proj1_sig z) (x b) == 0)%Q)). split; apply (ap_symmetric_unfolded Q_as_CSetoid); eapply Qlt_not_eq. apply Qlt_le_trans with (proj1_sig z). apply Qpos_ispos. apply Hn. apply Nat.le_trans with (Nat.max a n). auto with *. unfold m; auto with *. apply Qlt_le_trans with (proj1_sig z); auto with *. stepr ((/(Qmax (proj1_sig z) (x b))*/(x m))*(x m - (Qmax (proj1_sig z) (x b))))%Q; [| simpl; field; assumption]. stepl ((/ Qmax (proj1_sig z) (x b) * / x m)*((Qmax (proj1_sig z) (x b))*(x m)* proj1_sig e))%Q; [| simpl;field; assumption]. apply mult_resp_AbsSmall. assert (foo:forall q:Q, (0<=q -> 0<=/q)%Q). intros [[|p|p] q] qH; apply qH. apply mult_resp_nonneg. apply foo. apply Qle_trans with (proj1_sig z). apply Qpos_nonneg. apply Qmax_ub_l. apply foo. apply Qle_trans with (proj1_sig z). apply Qpos_nonneg. apply Hn. apply Nat.le_trans with (Nat.max a n); unfold m; auto with *. simpl in x_. apply (AbsSmall_leEq_trans _ (proj1_sig z*proj1_sig z*proj1_sig e)%Q). apply mult_resp_leEq_rht;[apply mult_resp_leEq_both|]; try apply Qpos_nonneg. apply Qmax_ub_l. apply Hn. apply Nat.le_trans with (Nat.max a n); unfold m; auto with *. assert (W:AbsSmall (R:=Q_as_COrdField) (proj1_sig z * proj1_sig z * proj1_sig e)%Q (x m - x b)%Q). apply Hb. apply Nat.le_trans with (Nat.max b c); unfold m; auto with *. apply Qmax_case;intros C;[|assumption]. apply leEq_imp_AbsSmall. unfold Qminus. rewrite <- Qle_minus_iff. apply Hn. apply Nat.le_trans with (Nat.max a n); unfold m; auto with *. apply Qle_trans with (x m - x b)%Q. rewrite -> Qle_minus_iff. stepr (proj1_sig z + - x b)%Q; [| simpl; ring]. rewrite <- Qle_minus_iff. assumption. destruct W; 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