proposition: Lemma exp_neq_0 : forall x:R, exp x <> 0.
proof: Proof. intro x. exact (not_eq_sym (Rlt_not_eq 0 (exp x) (exp_pos x))). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra