proposition: Lemma bigD_div_correct (x y : bigD) (k : Z) : Qball (2 ^ k) ('app_div x y k) ('x / 'y).
proof: Proof. assert (∀ xm xe ym ye : Z, (('xm * 2 ^ xe)%mc : Q) / (('ym * 2 ^ ye)%mc : Q) = ('xm * 2 ^ (-(k - 1) + xe - ye)) / 'ym * 2 ^ (k - 1)) as E1. intros. rewrite 2!int_pow_exp_plus by solve_propholds. rewrite dec_fields.dec_recip_distr. rewrite 2!int_pow_negate. transitivity (('xm / 'ym * 2 ^ xe / 2 ^ ye * (2 ^ (k - 1) / 2 ^ (k - 1)))%mc : Q); [| ring]. rewrite dec_recip_inverse by solve_propholds. ring. assert (∀ xm xe ym ye : Z, 'Z.div (Z.shiftl xm (-(k - 1) + xe - ye)) ym * 2 ^ (k - 1) - 2 ^ k ≤ ('xm * 2 ^ xe) / ('ym * 2 ^ ye : Q)) as Pleft. clear x y. assert (∀ z : Q, z * 2 ^ (k - 1) - 2 ^ k = ((z - 1) - 1) * 2 ^ (k - 1)) as E2. intros. mc_setoid_replace k with ((k - 1) + 1) at 2 by ring. rewrite (int_pow_exp_plus (k - 1)) by solve_propholds. ring_simplify. apply sm_proper. now rewrite commutativity. intros. rewrite E1, E2. apply (order_preserving (.* _)). apply rings.flip_le_minus_l. apply semirings.plus_le_compat_r; [easy |]. transitivity (('Z.shiftl xm (-(k - 1) + xe - ye) / 'ym - 1)%mc : Q). apply (order_preserving (+ -1)). now apply Qdiv_bounded_Zdiv. destruct (orders.le_or_lt 0 ym) as [E | E]. apply rings.flip_le_minus_l. apply semirings.plus_le_compat_r; [easy |]. apply (maps.order_preserving_flip_nonneg (.*.) (/ 'ym : Q)). apply dec_fields.nonneg_dec_recip_compat. now apply semirings.preserves_nonneg. now apply Qpow_bounded_Zshiftl. transitivity ((('Z.shiftl xm (-(k - 1) + xe - ye) + 1) / 'ym)%mc : Q). rewrite rings.plus_mult_distr_r. apply semirings.plus_le_compat; [reflexivity |]. rewrite rings.mult_1_l. apply rings.flip_le_negate. rewrite rings.negate_involutive, dec_fields.dec_recip_negate. apply dec_fields.flip_le_dec_recip_l; [solve_propholds |]. rewrite <-rings.preserves_negate. apply semirings.preserves_ge_1. apply rings.flip_le_negate. rewrite rings.negate_involutive. now apply nat_int.le_iff_lt_plus_1. apply semirings.flip_nonpos_mult_r. apply dec_fields.nonpos_dec_recip_compat. apply semirings.preserves_nonpos. now apply orders.lt_le. now apply orders.lt_le, Qpow_bounded_Zshiftl. assert (∀ xm xe ym ye : Z, ('xm * 2 ^ xe) / ('ym * 2 ^ ye : Q) ≤ '(Z.div (Z.shiftl xm (-(k - 1) + xe - ye)) ym) * 2 ^ (k - 1) + 2 ^ k) as Pright. clear x y. assert (∀ z : Q, z * 2 ^ (k - 1) + 2 ^ k = ((z + 1) + 1) * 2 ^ (k - 1)) as E2. intros. mc_setoid_replace k with ((k - 1) + 1) at 2 by ring. rewrite (int_pow_exp_plus (k - 1)) by solve_propholds. ring_simplify. apply sm_proper. now apply commutativity. intros. rewrite E1, E2. apply (order_preserving (.* _)). transitivity (('Z.shiftl xm (-(k - 1) + xe - ye) / 'ym + 1)%mc : Q). 2: now apply (order_preserving (+1)); apply orders.lt_le, Qdiv_bounded_Zdiv. destruct (orders.le_or_lt ym 0) as [E3 | E3]. apply semirings.plus_le_compat_r; [easy |]. apply semirings.flip_nonpos_mult_r. apply dec_fields.nonpos_dec_recip_compat. now apply semirings.preserves_nonpos. now apply Qpow_bounded_Zshiftl. transitivity ((('Z.shiftl xm (-(k - 1) + xe - ye) + 1) / ' ym)%mc : Q). apply (maps.order_preserving_flip_nonneg (.*.) ((/ 'ym)%mc : Q)). apply dec_fields.nonneg_dec_recip_compat. apply semirings.preserves_nonneg. now apply orders.lt_le. now apply orders.lt_le, Qpow_bounded_Zshiftl. rewrite rings.plus_mult_distr_r. apply semirings.plus_le_compat; [reflexivity |]. rewrite rings.mult_1_l. apply dec_fields.flip_le_dec_recip_l; [solve_propholds |]. apply semirings.preserves_ge_1. now apply nat_int.lt_iff_plus_1_le in E3. unfold cast. rewrite 3!inject_bigD_Q_correct. destruct x as [xm xe], y as [ym ye]. simpl. unfold cast, inject_bigZ_Q, cast, "∘". simpl. BigZ.zify. apply in_Qball. split. apply Pleft. apply Pright. 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