proposition: Lemma Qmult_AbsSmall : forall x y X Y : Q, QAbsSmall X x -> QAbsSmall Y y -> QAbsSmall (X*Y) (x*y).
proof: Proof. intros. apply AbsSmall_Qabs. rewrite Qabs_Qmult. apply (Qle_trans _ (X * Qabs y)). apply Qmult_le_compat_r. apply AbsSmall_Qabs in H. exact H. apply Qabs_nonneg. rewrite Qmult_comm, (Qmult_comm X). apply Qmult_le_compat_r. apply AbsSmall_Qabs in H0. exact H0. destruct H. apply (Qle_trans _ _ _ H) in H1. apply (Qplus_le_l _ _ X) in H1. ring_simplify in H1. apply (Qmult_le_l _ _ (2#1)). reflexivity. rewrite Qmult_0_r. exact H1. 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