proposition: Lemma Log_Exp : forall x H, Log (Exp x) H [=] x.
proof: Proof. intros x H. cut (Dom (Logarithm[o]Expon) x). intro H0. unfold Log in |- *; simpl in |- *; apply eq_transitive_unfolded with (Part _ _ H0). simpl in |- *; algebra. astepr (Part FId x I). apply Feq_imp_eq with realline. apply Log_Exp_inv. split. exists I. apply Log_domain. apply less_wdr with (Exp x); auto. simpl in |- *; algebra. Qed.
imports: CoRN.transc.TaylorSeries