proposition: Lemma bigQ_approx_Q_approx (x : bigQ) (k : Z) : 'app_approx x k = app_approx ('x) k.
proof: Proof. unfold app_approx, Q_approx, approximateQ, bigQ_approx. destruct k as [|p|]; try reflexivity. destruct x as [n|n d]; simpl. rewrite Z.div_1_r, Qmake_Qdiv. simpl. now rewrite Q.Zmult_Qmult, Qdiv_mult_l by auto with zarith. unfold cast, BigQ_Rationals.inject_QType_Q, BigQ.to_Q. case_eq (BigN.shiftl 1 (BigN.of_pos p) =? BigN.zero)%bigN; intros Ep. apply BigNeqb_correct, BigN.shiftl_eq_0_iff in Ep. discriminate. case_eq (d =? BigN.zero)%bigN; intros Ed. apply BigNeqb_correct in Ed. setoid_replace (BigZ.Pos d) with 0%bigZ by assumption. now rewrite BigZ.spec_div, Zdiv_0_r, Zmult_0_l. rewrite BigZ.spec_div, BigZ.spec_shiftl, Z.shiftl_mul_pow2 by apply BigN.spec_pos. rewrite BigN.spec_shiftl, Z.shiftl_1_l. replace (BigZ.to_Z (BigZ.Pos (BigN.of_pos p))) with (Zpos p) by (symmetry; apply BigN.spec_of_pos). rewrite BigN.spec_of_pos. replace (Z2P (2 ^ Zpos p)) with (2 ^ p)%positive by now rewrite <- Zpower_Ppow. rewrite <-Zpower_Ppow. rewrite Z2P_correct. reflexivity. apply orders.lt_iff_le_ne. split. now apply BigN.spec_pos. intros E. symmetry in E. change (d == BigN.zero)%bigN in E. apply BigN.eqb_eq in E. rewrite E in Ed. discriminate. 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