proposition: Lemma ln_scale_by_two_power : forall (n:Z) q (Hq:0 < q), (rational_ln_slow Hq + scale n ln2 == rational_ln_slow (ln_scale_by_two_power_adapt n Hq))%CR.
proof: Proof. intros n q Hq. rewrite -> ln2_correct. do 2 rewrite -> rational_ln_slow_correct'. rewrite <- CRmult_scale. rewrite <- IR_inj_Q_as_CR. rewrite <- IR_mult_as_CR. rewrite <- IR_plus_as_CR. apply IRasCR_wd. assert (X:[0][<](Two[//](two_ap_zero IR))[^^]n). apply zexp_pos. apply pos_two. stepl (Log _ (Qpos_adaptor Hq)[+]Log _ X). assert (Y:[0][<](inj_Q IR q)[*](Two[//](two_ap_zero IR))[^^]n). apply mult_resp_pos. apply (Qpos_adaptor Hq). assumption. stepl (Log _ Y). apply Log_wd. assert (Z:(inj_Q IR (2:Q))[#][0]). stepr (inj_Q IR (0:Q)). apply inj_Q_ap. discriminate. apply (inj_Q_nring IR 0). csetoid_replace ((Two[//]two_ap_zero IR)[^^](n)) (((inj_Q IR (2:Q))[//]Z)[^^]n). stepr (inj_Q IR q[*]inj_Q IR (2^n)). apply mult_wdr. apply eq_symmetric. apply inj_Q_power_Z. rstepl (inj_Q IR (2 ^ n)[*]inj_Q IR q). apply eq_symmetric. apply (inj_Q_mult IR (2^n) q). apply zexp_wd. apply eq_symmetric. apply (inj_Q_nring IR 2). apply Log_mult. apply bin_op_wd_unfolded. apply eq_reflexive. astepl ((zring n)[*]Log Two (pos_two IR)). apply mult_wdl. Transparent inj_Q. unfold inj_Q. simpl. rational. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRartanh_slow CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.tactics.Qauto CoRN.transc.Exponential CoRN.transc.ArTanH CoRN.tactics.CornTac