proposition: Lemma ARabs_AbsSmall : forall a b : AR, ARle (ARabs b) a <-> (ARle (-a) b /\ ARle b a).
proof: Proof. intros a b. pose proof CRabs_AbsSmall. split. - intro H6. assert ((CRabs (cast AR CR b) <= (cast AR CR a))%CR). { apply ARtoCR_preserves_le in H6. rewrite ARtoCR_preserves_abs in H6. exact H6. } specialize (H5 ('a) ('b)) as [H5 _]. specialize (H5 H7). split; apply ARtoCR_preserves_le. rewrite ARtoCR_preserves_opp. apply H5. apply H5. - intros [H6 H7]. apply (ARtoCR_preserves_le (-a) b) in H6. apply (ARtoCR_preserves_le b a) in H7. specialize (H5 ('a) ('b)) as [_ H5]. apply ARtoCR_preserves_le. rewrite ARtoCR_preserves_abs. apply H5. split. rewrite <- ARtoCR_preserves_opp. exact H6. exact H7. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRabs CoRN.reals.faster.ARArith