proposition: Lemma L1StepQPrelengthSpace : PrelengthSpace L1StepQ.
proof: Proof. intros x y e d1 d2 He Hxy. set (d:=(d1+d2)%Qpos) in *. simpl in *. unfold L1Ball in *. unfold L1Distance in *. pose (d1':=constStepF (proj1_sig d1)). pose (d2':=constStepF (proj1_sig d2)). pose (d':=constStepF ((/proj1_sig d))). set (f:=(d'*(x*d2' + y*d1'))%SQ). assert (X:(((d1' + d2')*d')==constStepF (1:QS))%SQ). { change (constStepF (proj1_sig (d1 + d2)%Qpos/proj1_sig (d1 + d2)%Qpos:QS)==constStepF (X:=QS) 1). apply constStepF_wd. simpl. field. intro. destruct d1, d2, e. simpl in H. simpl in He. rewrite H in He. exact (Qlt_irrefl 0 (Qlt_trans _ _ _ q1 He)). } exists (f). setoid_replace (x - f)%SQ with (d1' * d' * (x - y))%SQ. change ((d1' * d')%SQ * (x - y)%SQ) with (QscaleS (proj1_sig d1/ proj1_sig d)%Qpos ^@> (x-y)%SQ). rewrite -> L1Norm_scale. rewrite -> Qabs_pos; auto with *. unfold Qdiv. rewrite <- Qmult_assoc, <- (Qmult_comm (L1Norm (x-y))), Qmult_assoc. apply Qle_shift_div_r; auto with *. apply: mult_resp_leEq_lft; simpl; auto with *. apply Qle_trans with (proj1_sig e); auto with *. destruct d1,d. simpl. apply Qle_shift_div_l. exact q0. rewrite Qmult_0_l. apply Qlt_le_weak, q. setoid_replace (x - f) with (constStepF (1:QS)*x - f); [| simpl; ring]. rewrite <- X. unfold f. simpl; ring. setoid_replace (f -y) with (d2' * d' * (x - y))%SQ. change ((d2' * d')%SQ * (x - y)%SQ) with (QscaleS (proj1_sig d2/proj1_sig d)%Qpos ^@> (x-y)%SQ). rewrite -> L1Norm_scale. rewrite -> Qabs_pos; auto with *. unfold Qdiv. rewrite <- Qmult_assoc, <- (Qmult_comm (L1Norm (x-y))), Qmult_assoc. apply Qle_shift_div_r; auto with *. apply: mult_resp_leEq_lft; simpl;auto with *. apply Qle_trans with (proj1_sig e); auto with *. destruct d2,d. simpl. apply Qle_shift_div_l. exact q0. rewrite Qmult_0_l. apply Qlt_le_weak, q. setoid_replace (f- y) with (f - constStepF (1:QS)*y); [| simpl; ring]. rewrite <- X. unfold f. simpl. ring. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac