Require Export Wf_nat.
Require Export fun_aux.
Require Export sqrtrembase.
Section division.
Variable Zdivrem : Z -> Z -> Z * Z.
Definition Zquo := [a, b : ?] (Fst (Zdivrem a b)).
Definition Zmod := [a, b : ?] (Snd (Zdivrem a b)).
End division.
Section sq_fun.
Variable b' : Z.
Definition b := (Zmult (POS (xO xH)) b').
Variable b'Pos : (Zlt ZERO b').
Hints Resolve b'Pos :zarith.
Lemma bPos: (Zlt ZERO b).
Hints Resolve bPos .
Lemma bPowPos: (n : nat) (Zlt ZERO (pow b n)).
Hints Resolve bPowPos :zarith.
Definition sqrtrembase:
(n : Z)
(Zlt ZERO n) ->
(Zlt n (pow b (S (S O)))) ->
{p : Z * Z |
(Zplus (Zsquare (Fst p)) (Snd p)) = n /\
((Zle ZERO (Fst p)) /\
((Zle ZERO (Snd p)) /\ (Zle (Snd p) (Zmult (POS (xO xH)) (Fst p)))))}.
Lemma exponentbMulipleFour:
(h : nat)
(lt O h) ->
(Ex [v : Z] (Zmult (POS (xO (xO xH))) v) = (pow b (mult (S (S O)) h))).
Definition sqrt_F_type :=
[h : nat]
(n : Z)
(IsNormalized n (Zsquare (pow b h))) ->
{s : Z& {r : Z | (SqrtremProp n s r)}}.
Variable Zdivrem : Z -> Z -> Z * Z.
Variable
Zdivprop : (a, b : Z) (Zdivprop' a b (Zquo Zdivrem a b) (Zmod Zdivrem a b)).
Definition divrem': (n, m : Z) (Zle ZERO n) -> (Zlt ZERO m) -> (quotype n m).
Variable
simple_divrem : (n, m : Z) (Zle ZERO n) -> (Zlt ZERO m) -> (quotype n m).
Lemma normalized_positive:
(z : Z) (h : nat) (IsNormalized z (pow b h)) -> (Zle ZERO z).
Lemma normalized_base_case_aux:
(p : Z)
(Zle ZERO p) ->
(Zlt ZERO (Zplus (Zsquare p) (Zmult (POS (xO xH)) p))) -> (Zlt ZERO p).
Lemma normalized_base_case: (h : nat) (le h (S O)) -> (sqrt_F_type h).
Lemma pow_b_is_even:
(h : nat) (lt O h) -> (Ex [j : Z] <Z> ((pow b) h) = (Zmult (POS (xO xH)) j)).
Definition sqrt_F:
(h : nat) (f : (h' : nat) (lt h' h) -> (sqrt_F_type h')) (sqrt_F_type h).
Definition sqrtrem : (h : nat) (sqrt_F_type h) :=
(well_founded_induction nat lt lt_wf [x : nat] (sqrt_F_type x) sqrt_F).
End sq_fun.