proposition: Lemma Cauchy_IRasCR_is_Regular : forall (x:Cauchy_IR), is_RegularFunction Qball (Cauchy_IRasCR_raw x).
proof: Proof. intros [f Hf] e1 e2. simpl. destruct (Hf (proj1_sig e1) (Qpos_ispos e1)) as [n1 Hn1]. destruct (Hf (proj1_sig e2) (Qpos_ispos e2)) as [n2 Hn2]. cut (forall (e1 e2:Qpos) n1 n2, n2 <= n1 -> (forall m : nat, n1 <= m -> AbsSmall (R:=Q_as_COrdField) (proj1_sig e1) (f m[-]f n1)) -> (forall m : nat, n2 <= m -> AbsSmall (R:=Q_as_COrdField) (proj1_sig e2) (f m[-]f n2)) -> Qball (proj1_sig e1 + proj1_sig e2) (f n1) (f n2)). intros H. destruct (le_ge_dec n1 n2). eapply ball_sym;simpl. assert (QposEq (e1+e2) (e2+e1)) by (unfold QposEq; simpl; ring). apply (ball_wd _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. apply H; assumption. auto. clear - Hf. intros e1 e2 n1 n2 H Hn1 Hn2. assert (QposEq (e1+e2) (e2+e1)) by (unfold QposEq; simpl; ring). apply (ball_wd _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. eapply ball_weak. apply Qpos_nonneg. eapply Hn2. 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