fact: Definition ln (x:R) : R := match Rlt_dec 0 x with | left a => Rln (mkposreal x a) | right a => 0 end.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra