proposition: Lemma bigQ_approx_correct (x : bigQ) (k : Z) : Qball (2 ^ k) ('app_approx x k) ('x).
proof: Proof. rewrite bigQ_approx_Q_approx. now apply Q_approx_correct. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ Bignums.BigQ.BigQ CoRN.reals.fast.Compress CoRN.reals.faster.ARQ CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.reals.faster.ARArith MathClasses.implementations.stdlib_rationals MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.fast_rationals MathClasses.implementations.fast_integers