proposition: Lemma AbsSmall_Qabs : forall x y, (Qabs y <= x)%Q <-> QAbsSmall x y.
proof: Proof. cut (forall x y, (0 <= y)%Q -> ((Qabs y <= x)%Q <-> QAbsSmall x y)). intros H x y. generalize (H x y) (H x (-y)%Q). clear H. rewrite -> Qabs_opp. apply Qabs_case; intros H H1 H2. auto. assert (X:QAbsSmall x y <-> QAbsSmall x (- y)%Q). split. apply QAbsSmall_opp. intros X. unfold QAbsSmall. rewrite <- (Qopp_involutive y). apply QAbsSmall_opp. assumption. rewrite -> X. apply H2. rewrite -> Qle_minus_iff in H. ring_simplify in H. ring_simplify. apply H. intros x y H. rewrite -> Qabs_pos;[|assumption]. split. intros H0. split. 2 : exact H0. refine (Qle_trans _ 0 _ _ H). apply (Qopp_le_compat 0 x). exact (Qle_trans _ _ _ H H0). intros [_ H0]. assumption. 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