proposition: Theorem exp_Ropp : forall x:R, exp (- x) = / exp x.
proof: Proof. intros x; assert (H : exp x <> 0). - assert (H := exp_pos x); red; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). - apply Rmult_eq_reg_l with (r := exp x). + rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0. symmetry; apply Rinv_r. apply H. + apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra