proposition: Lemma EPrelengthSpace : PrelengthSpace X.
proof: Proof. Proof with auto with qarith. intros x y ε δ1 δ2 E F. pose (exist (Qlt 0) (1#2) eq_refl) as half. pose (exist (Qlt 0) (1#3) eq_refl) as third. simpl in *. assert (` ε < ` (δ1 + δ2)%Qpos)%Q as EE by (exact E). destruct (Qpos_sub _ _ EE) as [γ Eγ]. assert (1#3 < 1)%Q as G... pose proof (EPrelengthSpace_aux δ1 γ (1#3) G) as E1. pose proof (EPrelengthSpace_aux δ2 γ (1#3) G) as E2. destruct (@plY (f x) (f y) ε (exist _ _ E1) (exist _ _ E2)) as [z Ez1 Ez2]... - simpl. apply (Qlt_le_trans _ (`ε + (`γ - (2 # 3) * proj1_sig (Qpos_min γ (Qpos_min (Qpos_min (half * δ1 + half * δ2) (half * γ + half * δ2)) (half * δ1 + half * γ))))))%Q. rewrite <-(Qplus_0_r (`ε)) at 1. apply Qplus_lt_r. apply EPrelengthSpace_aux... do 5 rewrite Q_Qpos_min. simpl. rewrite <-Qmin_plus_distr_l. rewrite (Qmin_comm (`γ)). rewrite <-Qmin_assoc. setoid_replace (Qmin ((1 # 2) * ` δ1 + (1 # 2) * ` γ) (` γ)) with (Qmin ((1 # 2) * ` δ1 + (1 # 2) * ` γ) ((1#2) * ` γ + (1#2)*` γ)). rewrite <-Qmin_plus_distr_l. rewrite <-Qmin_plus_distr_r. repeat rewrite <-Qmin_mult_pos_distr_r... unfold Qminus. unfold QposEq in Eγ. rewrite (Qplus_assoc (` ε)), <- Eγ. simpl. ring_simplify. setoid_replace (-2#6) with (-1#3). apply Qle_refl. reflexivity. ring_simplify ((1 # 2) * ` γ + (1 # 2) * ` γ)%Q. reflexivity. - exists (app_inverse f z (exist (Qlt 0) (1#3) eq_refl * Qpos_min γ (Qpos_min δ1 δ2))). assert (QposEq δ1 (exist _ _ E1 + (third * Qpos_min δ1 γ))) by (unfold QposEq; simpl; ring). apply (Eball_wd _ _ _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. eapply ball_triangle; eauto. eapply ball_weak_le. 2: now apply ball_sym, dense_inverse. simpl. autorewrite with QposElim. apply Qmult_le_compat_l; eauto with qarith. assert (QposEq δ2 (third * Qpos_min δ2 γ + exist _ _ E2)) by (unfold QposEq; simpl; ring). apply (Eball_wd _ _ _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. eapply ball_triangle; eauto. eapply ball_weak_le. 2: now apply dense_inverse. simpl. autorewrite with QposElim. apply Qmult_le_compat_l; eauto with qarith. Qed.
imports: CoRN.metric2.Metric CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid CoRN.stdlib_omissions.Q CoRN.model.totalorder.QMinMax CoRN.metric2.Complete CoRN.metric2.Prelength MathClasses.interfaces.abstract_algebra