proposition: Lemma aq_abs : forall q:AQ, '(proj1_sig (abs_sig q)) == Qabs ('q).
proof: Proof. intro q. destruct (abs_sig q). unfold proj1_sig. destruct a. destruct aq_ring_morphism. destruct aq_order_embed. destruct semiringmor_plus_mor. destruct monmor_sgmor. destruct sgmor_setmor. assert (AQtoQ 0 == 0) by (apply rings.preserves_0). destruct (Qlt_le_dec ('q) 0). - rewrite Qabs_neg. rewrite <- aq_opp. apply sm_proper, H6. apply order_embedding_reflecting. rewrite H7. apply Qlt_le_weak, q0. apply Qlt_le_weak, q0. - rewrite Qabs_pos. 2: exact q0. apply sm_proper, H5. apply order_embedding_reflecting. rewrite H7. exact q0. 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