proposition: Lemma Log_resp_less : forall (x y : IR) Hx Hy, x [<] y -> Log x Hx [<] Log y Hy.
proof: Proof. intros x y Hx Hy H. unfold Log in |- *; apply Derivative_imp_resp_less with (openl [0]) I ( {1/} (Fid IR)); simpl in |- *; auto. apply Derivative_Log. intro contF. apply less_wdr with ([1][/] _[//]pos_ap_zero _ _ Hy). apply recip_resp_pos; auto. apply glb_charact. split. intros z Hz. elim Hz; intros t H1. elim H1; intros H2 H3. elim H3; clear Hz H1 H3; intros H1 H3. assert (H0 := H3 H1); simpl in H0. astepr ([1][/] t[//]ext2 (P:=fun _ : IR => True) H1). elim H2; intros HMin HMax. apply recip_resp_leEq; auto. apply less_leEq_trans with (Min x y); auto. apply less_Min; auto. apply leEq_wdr with (Max x y); auto. apply leEq_imp_Max_is_rht; apply less_leEq; auto. intros e He. exists ([1][/] _[//]pos_ap_zero _ _ Hy). exists y. split. split; [ apply Min_leEq_rht | apply rht_leEq_Max ]. repeat split. intro; simpl in |- *; apply pos_ap_zero; auto. simpl in |- *; algebra. astepl ZeroR; auto. Qed.
imports: CoRN.transc.TaylorSeries