proposition: Lemma Complete_located : forall (X : MetricSpace), locatedMetric X -> locatedMetric (Complete X).
proof: Proof. intros X Hx e d x y Hed. pose (d - e) as c. assert (0 < c) as Hc. { apply Qlt_minus_iff in Hed. exact Hed. } set (c':=((1#5)*exist _ _ Hc)%Qpos). assert (proj1_sig c'+e+ proj1_sig c' < e+(3#1)*proj1_sig c') as H. { rewrite -> Qlt_minus_iff. simpl. ring_simplify. apply (Qpos_ispos ((25#125)*exist _ _ Hc)). } destruct (Hx _ _ (approximate x c') (approximate y c') H) as [H0 | H0]. - left. rewrite <- ball_Cunit in H0. setoid_replace d with (proj1_sig c' + (e + (3#1) * proj1_sig c') + proj1_sig c')%Q by (simpl; unfold c; ring). eapply ball_triangle;[eapply ball_triangle;[|apply H0]|]; [apply ball_approx_r|apply ball_approx_l]. - right. abstract ( intros H1; apply H0; rewrite <- ball_Cunit; eapply ball_triangle;[eapply ball_triangle;[|apply H1]|]; [apply ball_approx_l|apply ball_approx_r]). Defined.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax