proposition: Lemma bigD_approx_correct (x : bigD) (k : Z) : Qball (2 ^ k) ('app_approx x k) ('x).
proof: Proof. setoid_replace (app_approx x k) with (app_div x 1 k). setoid_replace ('x : Q) with (('x / '1)%mc : Q). now apply bigD_div_correct. rewrite rings.preserves_1, dec_fields.dec_recip_1. now rewrite rings.mult_1_r. unfold app_div, bigD_div. simpl. rewrite BigZ.div_1_r. setoid_replace (-('k - 1) + expo x - 0) with (-('k - 1) + expo x); [reflexivity |]. now rewrite rings.negate_0, rings.plus_0_r. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ CoRN.model.totalorder.QposMinMax CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.util.Qdlog CoRN.reals.faster.ARArith MathClasses.theory.int_pow MathClasses.theory.nat_pow MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.interfaces.integers MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.fast_integers MathClasses.implementations.dyadics