proposition: Lemma ARabs_spec : ∀ x y : AR, (ARltS y x → False) ∧ (ARltS y (ARopp x) → False) ↔ (ARltS y (ARabs x) → False).
proof: Proof. intros x y. split. - intros [H6 H7]. apply (ARle_not_lt (ARabs x) y). apply (ARle_not_lt x y) in H6. apply (ARle_not_lt (ARopp x) y) in H7. pose proof (ARabs_AbsSmall y x) as [_ H5]. apply H5. split. 2: exact H6. rewrite <- (rings.negate_involutive x). apply rings.flip_le_negate. exact H7. - intro H6. apply (ARle_not_lt (ARabs x) y) in H6. pose proof (ARabs_AbsSmall y x) as [H5 _]. split. + apply (ARle_not_lt x y). apply H5. exact H6. + apply (ARle_not_lt (ARopp x) y). rewrite <- (rings.negate_involutive y). apply rings.flip_le_negate. apply H5, H6. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.reals.faster.ARArith CoRN.reals.faster.ARabs CoRN.metric2.Metric CoRN.metric2.Complete CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs ConstructiveFastReals