proposition: Lemma AbsSmall_Qabs : forall x y, (Qabs y <= x)%Q <-> AbsSmall x y.
proof: Proof. cut (forall x y, (0 <= y)%Q -> ((Qabs y <= x)%Q <-> AbsSmall (R:=Q_as_COrdField) 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:AbsSmall (R:=Q_as_COrdField) x y <-> AbsSmall (R:=Q_as_COrdField) x (- y)%Q). split. apply inv_resp_AbsSmall. intros X. stepr (- - y)%Q; [| simpl; ring]. apply inv_resp_AbsSmall. assumption. rewrite -> X. eapply 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. apply leEq_imp_AbsSmall; assumption. intros [_ H0]. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps