proposition: Lemma CRisCReals : is_CReals CRasCOrdField CRlim.
proof: Proof. split. intros [f Hf] e [d Hed]. destruct (Hf _ (CRlt_Qlt _ _ (Qpos_ispos ((1#2)*d)%Qpos))) as [n Hn]. exists n. intros m Hm. apply AbsSmall_leEq_trans with (inject_Q_CR (proj1_sig d)); [rstepr (e[-][0]);assumption|]. rewrite -> CRAbsSmall_ball. change (nat -> Complete Q_as_MetricSpace) in f. change (ball (proj1_sig d) (f m) (CRlim (Build_CauchySeq CRasCOrdField f Hf))). rewrite <- (MonadLaw5 (f m)). change (ball (proj1_sig d) (Cjoin (Cunit (f m))) (CRlim (Build_CauchySeq CRasCOrdField f Hf))). unfold CRlim. apply uc_prf. change (ball (proj1_sig d) (Cunit (f m)) (Build_RegularFunction (Rlim_subproof0 f Hf))). intros e1 e2. simpl. destruct (Hf (' proj1_sig e2)%CR (CRlt_Qlt _ _ (Qpos_ispos e2))) as [a Ha]. change (ball (proj1_sig (e1+d+e2)%Qpos) (f m) (f a)). destruct (le_ge_dec a m). rewrite <- CRAbsSmall_ball. eapply AbsSmall_leEq_trans;[|apply Ha;assumption]. intros x. autorewrite with QposElim. change (-proj1_sig x <= proj1_sig e1 + proj1_sig d + proj1_sig e2 - proj1_sig e2). rewrite -> Qle_minus_iff. ring_simplify. change (0<= proj1_sig (e1+d+x)%Qpos). apply Qpos_nonneg. apply ball_weak_le with (proj1_sig ((1#2)*d+(1#2)*d)%Qpos). rewrite -> Qle_minus_iff. simpl. ring_simplify. change (0<= proj1_sig (e1+e2)%Qpos). apply Qpos_nonneg. apply ball_triangle with (f n);[|apply ball_sym]; rewrite <- CRAbsSmall_ball; apply Hn. auto. apply Nat.le_trans with m; auto. intros x. assert (X:=(CR_b_upperBound (1#1) x)). destruct (CR_b (1 # 1) x) as [[n d] qpos]. destruct n as [|n|n]. inversion qpos. 2: inversion qpos. rewrite (anti_convert_pred_convert n) in X. exists (nat_of_P n)%nat. eapply leEq_transitive. apply X. clear X. intros z. simpl. unfold Cap_raw. simpl. apply Qle_trans with 0. rewrite -> Qle_minus_iff. ring_simplify. apply Qpos_nonneg. destruct (ZL4 n) as [a Ha]. rewrite Ha. clear Ha. simpl. unfold Cap_raw. simpl. rewrite <- Qle_minus_iff. remember ((1 # 2) * ((1 # 2) * z))%Qpos as q. simpl in Heqq. rewrite <- Heqq. clear Heqq. revert q. induction a; intro q. simpl. ring_simplify. unfold Qle. simpl. apply Zle_1_POS. simpl. unfold Cap_raw. simpl. rewrite -> Qle_minus_iff. rewrite <- Qplus_assoc. setoid_replace (1 + - (Pos.succ (Pos.of_succ_nat a) # d)) with (-((Pos.succ (Pos.of_succ_nat a) # d) - 1)) by ring. rewrite<- Qle_minus_iff. apply (Qle_trans _ (Pos.of_succ_nat a # d)). 2: apply IHa. generalize (P_of_succ_nat a). intros p. rewrite -> Qle_minus_iff. autorewrite with QposElim. replace RHS with (((p#d) + 1) + - (Pos.succ p # d)) by ring. rewrite <- Qle_minus_iff. unfold Qle. simpl. repeat rewrite Pmult_1_r. rewrite Pplus_one_succ_r. repeat rewrite Zpos_mult_morphism. apply Zmult_lt_0_le_compat_r. auto with *. repeat rewrite Zpos_plus_distr. auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRFieldOps CoRN.model.ordfields.CRordfield CoRN.reals.CReals CoRN.reals.fast.CRcorrect CoRN.model.metric2.Qmetric CoRN.tactics.CornTac