proposition: Lemma bigQ_div_correct (x y : bigQ) (k : Z) : Qball (2 ^ k) ('app_div x y k) ('x / 'y).
proof: Proof. mc_setoid_replace ('x / 'y : Q) with ('(x / y) : Q). now apply bigQ_approx_correct. now rewrite rings.preserves_mult, dec_fields.preserves_dec_recip. 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