proposition: Lemma QPrelengthSpace_help : forall (e d1 d2:Qpos), proj1_sig e < proj1_sig d1+ proj1_sig d2 -> forall (a b c:Q), ball (proj1_sig e) a b -> (c == (a*proj1_sig d2 + b*proj1_sig d1)/proj1_sig (d1+d2)%Qpos) -> ball (proj1_sig d1) a c.
proof: Proof. Proof with auto with *. intros e d1 d2 He a b c Hab Hc. simpl. unfold Qball. unfold QAbsSmall. rewrite Hc. clear Hc c. assert (0 < proj1_sig (d1 + d2)%Qpos). { apply (Qlt_trans _ (proj1_sig e)). destruct e. exact q. exact He. } split. - apply (Qmult_le_r _ _ (proj1_sig (d1+d2)%Qpos)). exact H. simpl. field_simplify. apply (Qle_trans _ (proj1_sig d1 * (-proj1_sig (d1 + d2)%Qpos))). simpl. field_simplify. apply Qle_refl. apply (Qle_trans _ (proj1_sig d1 * (a - b))). apply Qmult_le_l. destruct d1. exact q. destruct Hab. apply (Qle_trans _ (-proj1_sig e)). apply Qopp_le_compat, Qlt_le_weak, He. exact H0. field_simplify. apply Qle_refl. intro abs. destruct d1, d2. simpl in abs. simpl in H. rewrite abs in H. exact (Qlt_irrefl _ H). - apply (Qmult_le_r _ _ (proj1_sig (d1+d2)%Qpos)). exact H. simpl. field_simplify. apply (Qle_trans _ (proj1_sig d1 * (a-b))). field_simplify. apply Qle_refl. apply (Qle_trans _ (proj1_sig (d1 * (d1 + d2))%Qpos)). apply Qmult_le_l. destruct d1. exact q. destruct Hab. apply (Qle_trans _ (proj1_sig e)). exact H1. apply Qlt_le_weak, He. simpl. field_simplify. apply Qle_refl. intro abs. destruct d1,d2. simpl in H, abs. rewrite abs in H. exact (Qlt_irrefl _ H). Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals