Require Export pow.
Section ProofSqrt.
Implicit Arguments On.
Definition Zdivprop1' := [a, b, q, r : Z] a = (Zplus (Zmult q b) r).
Definition Zdivprop2' :=
[a, b, q : Z] (Zle ZERO a) -> (Zlt ZERO b) -> (Zle ZERO q).
Definition Zdivprop3' :=
[a, b, r : Z] (Zle ZERO a) -> (Zlt ZERO b) -> (Zle ZERO r).
Definition Zdivprop4' :=
[a, b, r : Z] (Zle ZERO a) -> (Zlt ZERO b) -> (Zlt r b).
Definition Zdivprop' :=
[a, b, q, r : Z]
(Zdivprop1' a b q r) /\
((Zdivprop2' a b q) /\ ((Zdivprop3' a b r) /\ (Zdivprop4' a b r))).
Tactic Definition divDefBreakdown2 def h0 :=
Elim def; Intros ddd1 ddd1'; Elim ddd1'; Intros h0 ddd2';
Clear ddd1 ddd1' ddd2'; Unfold Zdivprop2' in h0.
Tactic Definition divDefBreakdown3 def h0 :=
Elim def; Intros ddd1 ddd1'; Elim ddd1'; Intros ddd2 ddd2'; Elim ddd2';
Intros h0 ddd3'; Clear ddd1 ddd2 ddd1' ddd2' ddd3'; Unfold Zdivprop3' in h0.
Tactic Definition divDefBreakdown4 def h0 :=
Elim def; Intros ddd1 ddd1'; Elim ddd1'; Intros ddd2 ddd2'; Elim ddd2';
Intros ddd3 h0; Clear ddd1 ddd2 ddd1' ddd2' ddd3; Red in h0.
Definition IsNormalized :=
[N, H : Z] (Zle H (Zmult (POS (xO (xO xH))) N)) /\ (Zlt N H).
Variables N, L, R2, S2 : Z.
Variables H, Hhalf : Z.
Hypothesis Heven : H = (Zmult (POS (xO xH)) Hhalf).
Hypothesis Lpos : (Zlt ZERO L).
Hypothesis HL : (Zle L H).
Variables N', N'', N1, N0, Q, R'' : Z.
Variable N'N''def : (Zdivprop' N (Zsquare L) N' N'').
Variable N1N0def : (Zdivprop' N'' L N1 N0).
Variables S', R' : Z.
Variable
QR''def : (Zdivprop' (Zplus (Zmult R' L) N1) (Zmult (POS (xO xH)) S') Q R'').
Definition S1 := (Zplus (Zmult S' L) Q).
Definition R1 := (Zplus (Zmult R'' L) (Zminus N0 (Zsquare Q))).
Hypothesis H7
: (Zlt R1 ZERO) -> R2 = (Zplus R1 (Zminus (Zmult (POS (xO xH)) S1) (POS xH))).
Hypothesis H8 : (Zlt R1 ZERO) -> S2 = (Zminus S1 (POS xH)).
Hypothesis H9 : (Zle ZERO R1) -> R2 = R1.
Hypothesis H10 : (Zle ZERO R1) -> S2 = S1.
Definition SqrtremProp1 := [N, S, R : Z] N = (Zplus (Zsquare S) R).
Definition SqrtremProp2 := [N, S, R : Z] (Zle ZERO R).
Definition SqrtremProp3 := [N, S, R : Z] (Zle R (Zmult `2` S)).
Definition SqrtremProp4 := [N, S, R : Z] (Zlt ZERO S).
Definition SqrtremProp :=
[N, S, R : Z]
(SqrtremProp1 N S R) /\
((SqrtremProp2 N S R) /\ ((SqrtremProp3 N S R) /\ (SqrtremProp4 N S R))).
Hypothesis H11a : (SqrtremProp1 N' S' R').
Hypothesis H11b : (SqrtremProp2 N' S' R').
Hypothesis H11c : (SqrtremProp3 N' S' R').
Hypothesis H12 : (IsNormalized N (Zsquare (Zmult H L))).
Lemma Npos: (Zlt ZERO N).
Lemma Hpos: (Zlt ZERO H).
Hints Resolve Npos :sqrt.
Hints Resolve Lpos Hpos :sqrt.
Hints Resolve A1 A2 :sqrt.
Lemma N''pos: (Zle ZERO N'').
Lemma N0pos: (Zle ZERO N0).
Lemma R'pos: (Zle ZERO R').
Lemma L1: (Zle ZERO (Zplus (Zmult R' L) N1)).
Lemma Hhalfpos: (Zlt ZERO Hhalf).
Lemma normalized_positive_l: (Zle ZERO N ).
Lemma normalization_propagation:
(Zle (Zsquare H) (Zmult (POS (xO (xO xH))) N')).
Lemma former_prop4: (Zle H (Zmult (POS (xO xH)) S')).
Section H11d_required.
Hypothesis H11d : (SqrtremProp4 N' S' R').
Lemma R''pos: (Zle ZERO R'').
Lemma Qpos: (Zle ZERO Q).
Lemma Qge1: ~ Q = ZERO -> (Zle ZERO (Zminus Q (POS xH))).
Lemma L3: (Zle ZERO (Zplus (Zmult R'' L) N0)).
Lemma N1ltL: (Zlt N1 L).
Lemma QleL: (Zle Q L).
Lemma N0ltL: (Zlt N0 L).
Lemma T1_aux: (SqrtremProp1 N S1 R1).
Lemma T1: (SqrtremProp1 N S2 R2).
Lemma L2: (SqrtremProp2 N S2 R2).
Lemma S3: (SqrtremProp3 N S2 R2).
Lemma S2pos: (Zle ZERO S2).
Lemma S4: (SqrtremProp4 N S2 R2).
Lemma Sfinal: (SqrtremProp N S2 R2).
End H11d_required.
End ProofSqrt.