proposition: Lemma rational_ln_slow_correct : forall (a:Q) Ha Ha0, (@rational_ln_slow a Ha == IRasCR (Log (inj_Q IR a) Ha0))%CR.
proof: Proof. intros a Ha Ha0. unfold rational_ln_slow. assert (X:=artanh_DomArTanH (lnDomainAdaptor Ha)). rewrite -> (fun x => rational_artanh_slow_correct x X). rewrite <- CRmult_scale. rewrite <- IR_inj_Q_as_CR. rewrite <- IR_mult_as_CR. apply IRasCR_wd. csetoid_replace (inj_Q IR (2:Q)) (Two:IR); [|apply (inj_Q_nring IR 2)]. stepr (Two[*](Half[*]Log _ Ha0)); [|unfold Half; rational]. do 2 apply: mult_wdr. unfold Log. simpl. apply cspf_wd. set (b:=let (n, d) := a in (n - Zpos d) / (n + Zpos d)). assert (Y:inj_Q IR a[+][1][#][0]). apply Greater_imp_ap. apply plus_resp_pos; try assumption. apply pos_one. assert (Z:[1][-](inj_Q IR a[-][1][/]_[//]Y)[#][0]). apply Greater_imp_ap. rstepr (Two[/]_[//]Y). apply div_resp_pos. apply plus_resp_pos; try assumption. apply pos_one. apply pos_two. rstepr ([1][+](inj_Q IR a[-][1][/]_[//]Y)[/]_[//]Z). cut (inj_Q IR b[=](inj_Q IR a[-][1][/]inj_Q IR a[+][1][//]Y)). intros. apply div_wd; apply bin_op_wd_unfolded; try apply eq_reflexive; try apply un_op_wd_unfolded; assumption. stepr (inj_Q IR ((a-1)/(a+1))). apply inj_Q_wd. clear - Ha. destruct a as [n d]. simpl. unfold b. rewrite -> Qmake_Qdiv. field. split. unfold Qeq. auto with *. unfold Qeq, Qlt in *. simpl in *. intros H. apply (Zlt_not_le _ _ Ha). ring_simplify in H. ring_simplify. apply Z.le_trans with (-(d*1))%Z. 2: auto with *. apply Zle_left_rev. replace RHS with (-(n + (d*1)))%Z by ring. simpl. rewrite H. apply Z.le_refl. clear - Y. assert (X:inj_Q IR (a + 1)[#][0]). stepl (inj_Q IR a [+]inj_Q IR (nring 1)); [| now apply eq_symmetric; apply inj_Q_plus]. csetoid_rewrite (inj_Q_nring IR 1). rstepl (inj_Q IR a[+][1]). assumption. stepl (inj_Q IR (a - 1)[/]_[//]X); [| now apply eq_symmetric; apply inj_Q_div]. apply div_wd. stepl (inj_Q IR a[-]inj_Q IR 1); [| now apply eq_symmetric; apply inj_Q_minus]. apply bin_op_wd_unfolded. apply eq_reflexive. apply un_op_wd_unfolded. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). stepl (inj_Q IR a[+]inj_Q IR 1); [| now apply eq_symmetric; apply inj_Q_plus]. apply bin_op_wd_unfolded. apply eq_reflexive. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). 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