Require Export top_misc.
Require Export proof_sqrt.
Section top_sqrt.
Variable n:nat.
Hypothesis nle1 : (lt (1) n).
Hypothesis Hn_even : (even n).
Definition beta := (pow b n).
Lemma betaGt0 : `0 < beta`.
Hints Resolve betaGt0 : sqrt.
Lemma betaMultipleTwo : (Ex [beta' : Z] (Zmult `2` beta') = beta).
Hints Resolve betaMultipleTwo : sqrt.
Lemma powbetaGt0:(v:nat)`0<(pow beta v)`.
Hints Resolve powbetaGt0 : sqrt.
Variable nn : nat.
Variable Hnn : (lt O nn).
Variables Nt, St, Rt : Z.
Hypothesis Ntpos : (Zle ZERO Nt).
Hypothesis HNt : (Zle (pow beta (pred nn)) Nt) /\ (Zlt Nt (pow beta nn)).
Variable HighestLimb,Remainder : Z.
Hypothesis Hdivhighestlimb :
(Zdivprop' Nt (pow beta (pred nn)) HighestLimb Remainder).
Variable c':nat.
Hypothesis Hc' : (Zle (pow b (pred (minus n c'))) HighestLimb)
/\(Zlt HighestLimb (pow b (minus n c'))).
Hypothesis Hc'2 : (le O c')/\(lt c' n).
Definition c := (div2 c').
Definition tn := (div2 (S nn)).
Variables N1, S1, R1 : Z.
Hypothesis Hmpn_dq_sqrtrem : (IsNormalized N1 (pow beta (mult (2) tn))) ->
(SqrtremProp N1 S1 R1).
Lemma Ntstrictpos : (Zlt `0` Nt).
Lemma nn_even_implies_2tn_is_nn :
(even nn)->((mult (2) tn))=nn.
Hints Resolve nn_even_implies_2tn_is_nn : sqrt.
Lemma nn_odd_implies_2tn_is_nn :
(odd nn)->((mult (2) tn))=(S nn).
Hints Resolve nn_odd_implies_2tn_is_nn : sqrt.
Section easy_case.
Hypothesis already_normalized : ((even nn)/\(c=O))->N1=Nt/\S1=St/\R1=Rt.
Lemma implies_normalized : ((even nn)/\(c=O)) ->
(IsNormalized Nt (pow beta (mult (2) tn))).
Lemma already_normalized_ok : ((even nn)/\(c=O))->(SqrtremProp Nt St Rt).
End easy_case.
Section tough_case.
Hypothesis H' : (odd nn)\/(lt O c).
Hypothesis HNtN1 : (odd nn)\/(lt O c)->
N1=(Zmult (pow `2` (mult (2) c))
(Zmult (pow beta (minus (mult (2) tn) nn)) Nt)).
Lemma easy_thm1 : (Heven : (even nn))
(le n (plus (S (S O)) (plus (mult (S (S O)) c) (pred (minus n c'))))).
Lemma easy_thm2 : (le n (plus (S (S O)) (plus (mult (2) (div2 c')) (pred (minus n c'))))).
Lemma Ntsup :
`Nt < (pow beta (pred nn))*(pow b (minus n (mult (S (S O)) c)))`.
Lemma using_Ntsup : `(pow 2 (mult (S (S O)) c))*Nt < (pow beta nn)`.
Lemma implies_normalized_N1 : (IsNormalized N1 (pow beta (mult (2) tn))).
Lemma pow_beta_b : (e:nat)(pow beta e)=(pow b (mult n e)).
Definition k := (plus c (div2 (mult (minus (mult (S (S O)) tn) nn) n))).
Lemma N1_22k_Nt : `N1=(pow 2 (mult (S (S O)) k))*Nt`.
Variable q0,s0:Z.
Hypothesis Hs0 : (Zdivprop' S1 `(pow 2 k)` q0 s0).
Lemma Nts0 : `(pow 2 (mult (S (S O)) k))*Nt=(Zsquare (S1-s0))+2*S1*s0-(Zsquare s0)+R1`.
Variable R2:Z.
Hypothesis HR2:`R2=R1+2*S1*s0`.
Lemma thm_R2 : `(pow 2 (mult (S (S O)) k))*Nt=(Zsquare (S1-s0))-(Zsquare s0)+R2`.
Variable R3:Z.
Hypothesis HR3: `R3=R2-(Zsquare s0)`.
Lemma thm_R3 : `(pow 2 (mult (S (S O)) k))*Nt=(Zsquare (S1-s0))+R3`.
Lemma thm_q0s0 : `(S1-s0)=q0*(pow 2 k)`.
Variable Rdiv,Qdiv:Z.
Hypothesis HR : (Zdivprop' R3 `(pow 2 (mult (S (S O)) k))` Qdiv Rdiv).
Lemma div_rem_uniqueness : (p:nat)(W1,W2,W3:Z)(`0<=W3<(pow 2 p)`)->`(pow 2 p)*W1=(pow 2 p)*W2+W3`->`W3=0`.
Lemma thm_R3'' : `R3=(pow 2 (mult (S (S O)) k))*Qdiv`.
Lemma thm_between : `(Zsquare ((S1-s0)+s0))<=N1<(Zsquare ((S1-s0)+s0+1))`.
Lemma S1pos : (SqrtremProp N1 S1 R1)->
`0<S1`.
Lemma s0pos : (SqrtremProp N1 S1 R1)->
(Zdivprop' S1 (pow `2` k) q0 s0)->
`0<=s0`.
Lemma q0pos : (SqrtremProp N1 S1 R1)->
(Zdivprop' S1 (pow `2` k) q0 s0)->
`0<=q0`.
Lemma thm_between' :
`(Zsquare (q0*(pow 2 k)))<=N1<(Zsquare ((q0+1)*(pow 2 k)))`.
Lemma thm_topsqrtremprop1 : (SqrtremProp1 Nt q0 Qdiv).
Lemma thm_between_Nt : `(Zsquare q0) <= Nt < (Zsquare (q0 + 1))`.
Lemma thm_Qdiv2q0 : `Qdiv<=2*q0`.
Lemma thm_final : (SqrtremProp Nt q0 Qdiv).
End tough_case.
End top_sqrt.