proposition: Lemma ln_correct : forall prec, extension ln (I.ln prec).
proof: Proof. intros prec xi x Hx. generalize (I.ln_correct prec xi _ Hx). unfold Xln', Xbind. case is_positive ; try easy. now case I.convert. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic