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