Require Export Wf_nat.
Require Export proof_sqrt.
Require Export div2.
Inductive quotype [n, m : Z] : Set :=
quo_type_def: (q, r : Z) (Zdivprop' n m q r) -> (quotype n m) .
Lemma normalized_divide:
(H', L, n, n1, n2 : Z)
(Zlt ZERO L) ->
(Zle L (Zmult (POS (xO (xO xH))) H')) ->
(Zle ZERO n) ->
(Zdivprop' n L n1 n2) ->
(IsNormalized n (Zmult (Zmult (POS (xO (xO xH))) H') L)) ->
(IsNormalized n1 (Zmult (POS (xO (xO xH))) H')).
Lemma exponentbMulipleFour:
(h : nat)
(b' : Z)
(lt O h) ->
(Ex [v : Z]
(Zmult (POS (xO (xO xH))) v) =
(pow (Zmult (POS (xO xH)) b') (mult (S (S O)) h))).
Lemma normalized_div2:
(h, l, h' : nat)
(b', n, n1, n2 : Z)
(Zlt ZERO b') ->
(Zlt ZERO n) ->
(lt O h) ->
(Zdivprop' n (pow (Zmult (POS (xO xH)) b') (mult (S (S O)) l)) n1 n2) ->
l = (floordiv2 h) ->
(mult (S (S O)) h') = h \/ (mult (S (S O)) h') = (plus h (S O)) ->
(IsNormalized n (pow (Zmult (POS (xO xH)) b') (mult (S (S O)) h))) ->
(IsNormalized n1 (pow (Zmult (POS (xO xH)) b') (mult (S (S O)) h'))).
Definition S2 : Z -> Z -> Z -> Z -> Z -> Z :=
[L, N0, Q, S', R'' : Z]
( Case (Z_le_lt_dec (R1 L N0 Q R'') ZERO) of
[Hge : ?] (S1 L Q S') [Hlt : ?] (Zminus (S1 L Q S') (POS xH)) end ).
Lemma S2_eq1:
(L, N0, Q, S', R'' : Z)
(Zle ZERO (R1 L N0 Q R'')) -> (S2 L N0 Q S' R'') = (S1 L Q S').
Lemma S2_eq2:
(L, N0, Q, S', R'' : Z)
(Zlt (R1 L N0 Q R'') ZERO) ->
(S2 L N0 Q S' R'') = (Zminus (S1 L Q S') (POS xH)).
Definition R2 : Z -> Z -> Z -> Z -> Z -> Z :=
[L, N0, Q, S', R'' : Z]
( Case (Z_le_lt_dec (R1 L N0 Q R'') ZERO) of
[Hge : ?] (R1 L N0 Q R'')
[Hlt : ?]
(Zplus
(R1 L N0 Q R'') (Zminus (Zmult (POS (xO xH)) (S1 L Q S')) (POS xH)))
end ).
Lemma R2_eq1:
(L, N0, Q, S', R'' : Z)
(Zle ZERO (R1 L N0 Q R'')) -> (R2 L N0 Q S' R'') = (R1 L N0 Q R'').
Lemma R2_eq2:
(L, N0, Q, S', R'' : Z)
(Zlt (R1 L N0 Q R'') ZERO) ->
(R2 L N0 Q S' R'') =
(Zplus (R1 L N0 Q R'') (Zminus (Zmult (POS (xO xH)) (S1 L Q S')) (POS xH))).
Hints Resolve S2_eq1 S2_eq2 R2_eq1 R2_eq2 .
Inductive nat_half_decompose [n : nat] : Set :=
c_decompose:
(h, l : nat)
(plus h l) = n ->
(lt h n) -> (lt O l) -> (le l h) -> (nat_half_decompose n) .
Theorem le_ceildiv2': (n : nat) (le (ceildiv2' n) n).
Hint arith := Resolve le_ceildiv2'.
Theorem lt_ceildiv2': (n : nat) (lt (S O) n) -> (lt (ceildiv2' n) n).
Theorem lt_floordiv: (n : nat) (lt (S O) n) -> (lt O (floordiv2 n)).
Definition decompose: (n : nat) (lt (S O) n) -> (nat_half_decompose n).