proposition: Lemma invnz_correct : forall prec xi x, x <> 0%R -> contains (I.convert xi) (Xreal x) -> contains (I.convert (I.invnz prec xi)) (Xreal (/ x)).
proof: Proof. intros prec xi x Zx Hx. refine (_ (I.invnz_correct prec xi _ _ Hx)). unfold Xinv', Xbind. now rewrite is_zero_false. contradict Zx. now injection Zx. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic