proposition: Lemma exp_pos : forall x:R, 0 < exp x.
proof: Proof. intro; destruct (total_order_T 0 x) as [[Hlt|<-]|Hgt]. - apply (exp_pos_pos _ Hlt). - rewrite exp_0; apply Rlt_0_1. - replace (exp x) with (1 / exp (- x)). + unfold Rdiv; apply Rmult_lt_0_compat. * apply Rlt_0_1. * apply Rinv_0_lt_compat; apply exp_pos_pos. apply (Ropp_0_gt_lt_contravar _ Hgt). + cut (exp (- x) <> 0). * intro; unfold Rdiv; apply Rmult_eq_reg_l with (exp (- x)). -- rewrite Rmult_1_l; rewrite Rinv_r. ++ rewrite <- exp_plus. rewrite Rplus_opp_l; rewrite exp_0; reflexivity. ++ apply H. -- apply H. * assert (H := exp_plus x (- x)). rewrite Rplus_opp_r in H; rewrite exp_0 in H. red; intro; rewrite H0 in H. rewrite Rmult_0_r in H. elim R1_neq_R0; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra