proposition: Lemma EPrelengthSpace_aux (x y : Qpos) (z : Q) : (z < 1 → 0 < proj1_sig x - z * proj1_sig (Qpos_min x y))%Q.
proof: Proof. Proof with auto. intros E. apply (proj1 (Qlt_minus_iff _ _)). destruct (Qle_total (`y) (`x)) as [F|F]. pose proof (proj1 (Qpos_le_min_r x y) F). unfold QposEq in H0. rewrite H0. apply Qlt_le_trans with (`y)... apply Qpos_lt_1_mult_l... pose proof (proj1 (Qpos_le_min_l x y) F). unfold QposEq in H0. rewrite H0. apply Qpos_lt_1_mult_l... 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