proposition: Lemma abs_div_aqtoq_shift : forall (q r s : AQ), 0 < r -> (Qabs (AQtoQ q / AQtoQ r) <= AQtoQ s <-> le (abs q) (r * s)).
proof: Proof. assert (forall q:AQ, Qabs (AQtoQ q) == AQtoQ (abs q)) as preserves_abs. { intros. rewrite abs.preserves_abs. reflexivity. } assert (forall q r:AQ, AQtoQ (q*r) == AQtoQ q*AQtoQ r) as preserves_mult. { intros. rewrite rings.preserves_mult. reflexivity. } intros. assert (0 < AQtoQ r). { rewrite <- rings.preserves_0. destruct aq_strict_order_embed. apply strict_order_embedding_preserving. exact H5. } split. - intros. unfold Qdiv in H7. rewrite Qabs_Qmult, Q.Qabs_Qinv in H7. rewrite (Qabs_pos (AQtoQ r)) in H7. rewrite preserves_abs, Qmult_comm in H7. apply (Qmult_le_l _ _ (AQtoQ r)) in H7. 2: exact H6. rewrite Qmult_assoc, Qmult_inv_r, Qmult_1_l in H7. rewrite <- preserves_mult in H7. destruct aq_order_embed, order_embedding_reflecting. apply order_reflecting in H7. exact H7. intro abs. rewrite abs in H6. exact (Qlt_irrefl 0 H6). apply Qlt_le_weak, H6. - intros. unfold Qdiv. rewrite Qabs_Qmult, Q.Qabs_Qinv. rewrite (Qabs_pos (AQtoQ r)). rewrite preserves_abs. rewrite Qmult_comm. apply (Qmult_le_l _ _ (AQtoQ r)). exact H6. rewrite Qmult_assoc, Qmult_inv_r, Qmult_1_l. rewrite <- preserves_mult. destruct aq_order_embed. apply order_embedding_preserving. exact H7. intro abs. rewrite abs in H6. exact (Qlt_irrefl 0 H6). apply Qlt_le_weak, H6. Qed.
imports: Coq.QArith.Qabs CoRN.util.Qdlog CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.model.reals.CRreal CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.ARArith