proposition: Lemma AQabs_triangle_reverse : forall a b : AQ, Qabs (' AQabs a - ' AQabs b) <= Qabs ('a - 'b).
proof: Proof. intros a b. unfold AQabs. rewrite aq_abs, aq_abs. apply Qabs_case. - intros _. apply Qabs_triangle_reverse. - intros. apply (Qle_trans _ (Qabs ('b) - Qabs ('a))). ring_simplify; apply Qle_refl. rewrite <- (Qabs_opp (' a - ' b)). setoid_replace (- (' a - ' b))%Q with (' b - ' a)%Q. apply Qabs_triangle_reverse. unfold equiv, stdlib_rationals.Q_eq. ring. 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