proposition: Lemma CRstandard_regular : forall (xn : nat -> CR) (xncau : CRcauchy_sequence xn), is_RegularFunction (@ball CR) (CRstandard_modulus xn xncau).
proof: Proof. intros xn xncau e1 e2. apply CRabs_ball. unfold CRstandard_modulus. destruct (le_ge_dec (proj1_sig (xncau (proj1_sig (Qarchimedean_le (/ proj1_sig e1))))) (proj1_sig (xncau (proj1_sig (Qarchimedean_le (/ proj1_sig e2)))))). - destruct (xncau (proj1_sig (Qarchimedean_le (/ proj1_sig e1)))) as [n H]. simpl in l. destruct e1 as [e1 e1pos]. destruct e2 as [e2 e2pos]. unfold proj1_sig. specialize (H n _ (Nat.le_refl _) l). apply CRle_not_lt in H. apply (CRle_trans H). clear H. apply CRle_Qle. unfold proj1_sig. destruct (Qarchimedean_le (/ e1)) as [p H]. apply (Qle_trans _ (e1+0)). 2: apply Qplus_le_r, Qlt_le_weak, e2pos. rewrite Qplus_0_r. apply (Qmult_le_l _ _ e1) in H. 2: exact e1pos. rewrite Qmult_inv_r in H. change (1#p) with (/(Z.pos p#1)). apply Qle_shift_inv_r. reflexivity. apply H. apply (Qpos_nonzero (exist _ e1 e1pos)). - destruct (xncau (proj1_sig (Qarchimedean_le (/ proj1_sig e2)))) as [n H]. simpl in g. destruct e1 as [e1 e1pos]. destruct e2 as [e2 e2pos]. unfold proj1_sig. specialize (H _ n g (Nat.le_refl _)). apply CRle_not_lt in H. apply (CRle_trans H). clear H. apply CRle_Qle. unfold proj1_sig. destruct (Qarchimedean_le (/ e2)) as [p H]. apply (Qle_trans _ (0+e2)). 2: apply Qplus_le_l, Qlt_le_weak, e1pos. rewrite Qplus_0_l. apply (Qmult_le_l _ _ e2) in H. 2: exact e2pos. rewrite Qmult_inv_r in H. change (1#p) with (/(Z.pos p#1)). apply Qle_shift_inv_r. reflexivity. apply H. apply (Qpos_nonzero (exist _ e2 e2pos)). Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon