Require Export Zextensions.
Require Export compute_POS.
Require Export ZArithRing.
Require Export Omega.
Inductive sqrt_data [n : Z] : Set :=
c_sqrt:
(s, r : Z)
<Z> n = (Zplus (Zmult s s) r) ->
(Zle ZERO r) /\ (Zle r (Zmult (POS (xO xH)) s)) -> (sqrt_data n) .
Definition sqrtrempos: (p : positive) (sqrt_data (POS p)).