proposition: Lemma Qmult_uc_prf (c:Qpos) : @is_UniformlyContinuousFunction Q_as_MetricSpace (Q_as_MetricSpace --> Q_as_MetricSpace) (fun a:Q => uc_compose (Qscale_uc a) (QboundAbs c)) (Qmult_modulus c).
proof: Proof. Proof with simpl in *; auto with *. intros e a0 a1 H. split. apply Qpos_nonneg. intro b. simpl in *. set (b' := Qmax (- proj1_sig c) (Qmin (proj1_sig c) b)). repeat rewrite -> (fun x => Qmult_comm x b'). apply Qscale_uc_prf. assert (QposEq (e * Qpos_inv c) (Qpos_inv c*e)%Qpos) by (unfold QposEq; simpl; ring). apply (ball_wd _ H0 _ _ (reflexivity _) _ _ (reflexivity _)) in H. clear H0. apply ball_ex_weak_le with (Qpos_inv c*e)%Qpos;[|assumption]. unfold b'. destruct c as [[cn cd] cpos]. destruct cn as [|cn|cn]. inversion cpos. 2: inversion cpos. apply Qmax_case. intros. apply Qle_refl. simpl. apply Qmin_case. intros. apply Qle_refl. intros H1 H2. destruct b as [[|bn|bn] bd]... - apply Qmult_le_r. destruct e; exact q. apply Qle_shift_inv_r. reflexivity. rewrite <- Qmult_1_l in H1. apply Qle_shift_div_l in H1. apply (Qle_trans _ _ _ H1). rewrite Qmult_comm. apply Qmult_le_l. reflexivity. apply Z.le_refl. reflexivity. - apply Qmult_le_r. destruct e; exact q. apply Qle_shift_inv_r. reflexivity. apply Qopp_le_compat in H2. rewrite Qopp_involutive in H2. rewrite <- Qmult_1_l in H2. apply Qle_shift_div_l in H2. 2: reflexivity. apply (Qle_trans _ _ _ H2). rewrite Qmult_comm. apply Qmult_le_l. reflexivity. apply Z.le_refl. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names