proposition: Lemma Exp_Log : forall x H, Exp (Log x H) [=] x.
proof: Proof. intros x H. set (y := Exp (Log x H)) in *. cut ([0] [<] y); [ intro H0 | unfold y in |- *; apply Exp_pos ]. cut (Log y H0 [=] Log x H); [ intro H1 | unfold y in |- *; algebra ]. cut ([0] [=] Log y H0[-]Log x H); [ clear H1; intro H1 | apply eq_symmetric_unfolded; apply x_minus_x; auto ]. apply leEq_imp_eq. apply Exp_Log_lemma with H H0; auto. apply Exp_Log_lemma with H0 H. astepl ( [--]ZeroR); rstepr ( [--] (Log y H0[-]Log x H)); algebra. Qed.
imports: CoRN.transc.TaylorSeries