proposition: Lemma CompletePL : forall X, PrelengthSpace X -> PrelengthSpace (Complete X).
proof: Proof. intros X Xpl x y e d1 d2 He Hxy. destruct (Qpos_sub _ _ He) as [x0 q]. pose (exist (Qlt 0) (4#1) eq_refl) as four. pose (exist (Qlt 0) (1#5) eq_refl) as fifth. pose (gA := (fifth*x0)%Qpos). pose (g := Qpos_min (Qpos_min ((1#2)*d1) ((1#2)*d2)) gA). unfold PrelengthSpace in Xpl. assert (Hd1: proj1_sig g < proj1_sig d1). { unfold g. eapply Qle_lt_trans. apply Qpos_min_lb_l. eapply Qle_lt_trans. apply Qpos_min_lb_l. simpl. rewrite <- (Qmult_1_l (proj1_sig d1)). rewrite Qmult_assoc. apply Qmult_lt_r. apply Qpos_ispos. reflexivity. } assert (Hd2: proj1_sig g < proj1_sig d2). { unfold g. eapply Qle_lt_trans. apply Qpos_min_lb_l. eapply Qle_lt_trans. apply Qpos_min_lb_r. simpl. rewrite <- (Qmult_1_l (proj1_sig d2)). rewrite Qmult_assoc. apply Qmult_lt_r. apply Qpos_ispos. reflexivity. } destruct (Qpos_sub _ _ Hd1) as [d1' Hd1']. destruct (Qpos_sub _ _ Hd2) as [d2' Hd2']. assert (He': proj1_sig (g + e + g)%Qpos < proj1_sig (d1' + d2')%Qpos). { simpl. apply (Qplus_lt_l _ _ (proj1_sig g+ proj1_sig g)). setoid_replace (proj1_sig d1' + proj1_sig d2' + (proj1_sig g + proj1_sig g)) with (proj1_sig ((g+d1')%Qpos) + proj1_sig (g+d2')%Qpos) by (simpl; ring). unfold QposEq in *. rewrite <- Hd1'. rewrite <- Hd2'. clear d1' Hd1' d2' Hd2'. apply Qle_lt_trans with (proj1_sig (e + four*gA)%Qpos). apply (Qle_trans _ (proj1_sig e+(4#1)*proj1_sig g)). ring_simplify. apply Qle_refl. apply Qplus_le_r. apply Qmult_le_l. reflexivity. apply Qpos_min_lb_r. rewrite -> q. apply Qplus_lt_r. simpl. rewrite Qmult_assoc, <- (Qmult_1_l (proj1_sig x0)), Qmult_assoc. apply Qmult_lt_r. destruct x0; exact q0. reflexivity. } destruct (Xpl _ _ _ _ _ He' (Hxy g g)) as [c Hc1 Hc2]. exists (Cunit c). rewrite Hd1'. eapply ball_triangle. apply ball_approx_r. rewrite -> ball_Cunit. assumption. rewrite Hd2'. rewrite Qplus_comm. eapply ball_triangle with (Cunit (approximate y g)). rewrite -> ball_Cunit. assumption. apply ball_approx_l. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.List CoRN.stdlib_omissions.Q