proposition: Lemma div_correct : forall prec, extension_2 Rdiv (I.div prec).
proof: Proof. intros prec xi yi x y Hx Hy. generalize (I.div_correct prec _ _ _ _ Hx Hy). simpl. unfold Xdiv'. case is_zero ; try easy. now case I.convert. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic