proposition: Lemma Qplus_uc_uncurry : is_UniformlyContinuousFunction (fun ab : ProductMS Q_as_MetricSpace Q_as_MetricSpace => fst ab + snd ab) (fun e => (1#2)*e)%Qpos.
proof: Proof. intros e1 [a b] [c d] [H H0]. simpl. simpl in H, H0. apply AbsSmall_Qabs. setoid_replace (a + b - (c + d))%Q with (a - c + (b - d)) by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ (Qabs_triangle _ _)). apply (Qle_trans _ ((1#2)*`e1 + (1#2)*`e1)). apply Qplus_le_compat. - apply AbsSmall_Qabs in H. apply H. - apply AbsSmall_Qabs in H0. apply H0. - ring_simplify. apply Qle_refl. Qed.
imports: QArith Qabs CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.totalorder.QMinMax CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.stdlib_omissions.Pair MathClasses.interfaces.canonical_names