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