proposition: Lemma gball_complete (r : Q) (x y : Complete X) : ball r x y <-> forall e1 e2 : Qpos, ball (proj1_sig e1 + r + proj1_sig e2)%mc (approximate x e1) (approximate y e2).
proof: Proof. destruct (Qsec.Qdec_sign r) as [[r_neg | r_pos] | r_zero]. + split; intro H; [exfalso | exact H]. apply (Qlt_not_le _ _ r_neg). assert (H1 : 0 < -(r / 3)) by (apply Q.Qopp_Qlt_0_l, Q.Qmult_neg_pos; auto with qarith). specialize (H (exist _ _ H1) (exist _ _ H1)); simpl in H. mc_setoid_replace (- (r / 3) + r + - (r / 3)) with (r / 3) in H by (field; discriminate). apply (msp_nonneg (msp X)) in H. apply (Qmult_le_r _ _ (1#3)). reflexivity. rewrite Qmult_0_l. exact H. + simpl; unfold regFunBall. split; intros H e1 e2. - specialize (H e1 e2). apply H. - apply H. + rewrite r_zero. simpl; unfold regFunEq. split; intros H e1 e2; specialize (H e1 e2). - rewrite r_zero, Qplus_0_r. rewrite Qplus_0_r in H. exact H. - rewrite Qplus_0_r. rewrite r_zero, Qplus_0_r in H. exact H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.metric2.Metric CoRN.ode.metric CoRN.model.totalorder.QposMinMax MathClasses.interfaces.abstract_algebra MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.orders.orders MathClasses.orders.semirings MathClasses.orders.rings MathClasses.theory.rings