Require Export div2.
Require Export mpn_complements.
Fixpoint div2' [n:nat] : nat :=
Cases n of O => O
| (S p) => Cases p of O =>O
| (S q) => (S (div2' q))
end
end.
Theorem div2_le : (n:nat)(le (div2' n) n).
Lemma div2_minus :
(n:nat)(minus (S (S n)) (div2' (S (S n))))=(minus (S n) (div2' n)).
Lemma div2_minus_lt : (n:nat)(lt (0) n)->(lt (0) (minus n (div2' n))).
Lemma lt_O_div2 :(n:nat)(lt (1) n)->(lt (O) (div2' n)).
Lemma lt_minus_div2 : (n:nat)(lt (1) n)->(lt (minus n (div2' n)) n).
Lemma div2_floordiv2_equal : (n:nat)(div2' n)=(floordiv2 n).
Lemma two_step_ind : (P:nat->Prop)(P O)->(P (S O))->((n:nat)(P n)->(P (S (S n))))->(n:nat)(P n).
Lemma minus_div2_S : (n:nat)(S (minus n (div2' n)))=(minus (S (S n)) (div2' (S (S n)))).
Lemma div2_minus' : (n:nat) (mult (2) (minus n (div2' n)))=n
\/(mult (2) (minus n (div2' n)))=(plus n (1)).
Lemma div2_mult2 : (n:nat)(mult (2)(div2' n))=n\/(plus (mult(2)(div2' n)) (1))=n.
Lemma div2_odd : (n:nat)~(div2' n)=(minus n (div2' n))->
(plus (mult (2) (div2' n)) (1)) = n.
Lemma inj_minus_div2 :
(n:nat)(inject_nat (minus n (div2' n)))=`(inject_nat n)-(inject_nat (div2' n))`.
Lemma div2_double_le : (n:nat)(le (mult (2) (div2' n)) n).
Lemma div2_nn_l :(nn:nat)(lt (1) nn)->(lt (0) (div2' nn)).
Lemma one_le_minus_div2 :
(n:nat)(lt (1) n) -> (le (1)(minus n (div2' n))).
Lemma le_div2_minus : (n:nat)(le (div2' n)(minus n (div2' n))).
Lemma two_2 : (n:Z)(`2*n`)=`n+n`.
Theorem Zminus_permute : (c,b,a:Z)`a-b-c=a-c-b`.
Theorem Zminus_plus_permute : (c,b,a:Z)`a+b-c=a-c+b`.
Theorem Zplus_minus_assoc : (a,b,c:Z) `a+(b-c)=a+b-c`.
Theorem Zminus_plus_assoc : (a,b,c:Z)`a-(b+c)=(a-b)-c`.
Theorem Zminus_minus_assoc : (a,b,c:Z)`a-(b-c)=(a-b)+c`.
Theorem Zminus_permute_square : (c,b,a:Z)`a-b-(c*c)=a-(c*c)-b`.
Theorem Zminus_plus_permute_square : (c,b,a:Z)`a+b-(c*c)=a-(c*c)+b`.
Lemma I_decompose_divprop :
(m:(array bound modZ); pos,l,h,n:nat)
n=(plus l h) ->
(Zdivprop' (I m pos n) (pow beta l) (I m (plus pos l) h)(I m pos l)).
Lemma square_monotone : (x,y:Z)`0 <= x`->`x<=y`->`x*x<=y*y`.
Lemma add_pos_le : (x,y:Z)`0<=y` -> `x<=x+y`.
Theorem Zplus_minus2 : (x,y,z:Z)`x=z-y`->`x+y=z`.
Theorem pow_div2 : (n:nat)`(pow beta (div2' n))*(pow beta (minus n (div2' n)))=
(pow beta n)`.
Lemma Hhalf_easy : (nn0:nat)
(lt (0) nn0)-> (EX Hhalf:Z | `2*Hhalf` = (pow beta (minus nn0 (div2' nn0)))).
Theorem between_0_1 : (x:Z)`-1<x<=1`->`x=0`\/`x=1`.
Theorem between_0_1' : (x:Z) `0<=x<=1` -> `x=0`\/`x=1`.
Theorem square_positive : (x:Z)`0 <= x*x`.
Theorem Zlt_mult_r : (a,b,c:Z)`0<a`->`b<c`->`b*a<c*a`.
Theorem Zlt_mult_l : (a,b,c:Z)`0<a`->`b<c`->`a*b<a*c`.
Theorem aux_1 : (n,p1,p2,p3:nat)(m1,m2,m3:(array bound modZ))
`(pow beta n)+2*((I m1 p1 (minus n (div2' n)))*(pow beta (div2' n))+(I m2 p2 (div2' n)) )-1<=
2*(pow beta n)+((I m3 p3 n)+(pow beta n))`.
Theorem aux_2 : (n,p1,p2,p3:nat)(m1,m2,m3:(array bound modZ))
`(I m2 p2 n)+2*((I m1 p1 (minus n (div2' n)))+1)*(pow beta (div2' n))-1 <
2*(pow beta n)+((I m3 p3 n)+(pow beta n))`.
Theorem aux_3 : (x:Z)`0<x`->`1<=x`.
Theorem aux_4 : (x,y:Z)`x < 2` -> `-1 < x + y` -> `-1 <= y`.
Theorem aux_5 : (x,y:Z)`y=(-x)` -> `x <= 0` -> `-1 <= x` -> `y=0`\/`y=1`.
Theorem aux_6 : (x,y:Z) `y<x` -> `(-1)*x<0-y`.
Theorem aux_7 : (x,y:Z)`x<y` -> `x+(-1)*y < 0`.
Theorem aux_8 : (x,y:Z)`0<=x`->`y-x<=y`.
Theorem aux_10 : (x,y:Z)`0<=x` -> `y <= y + x`.
Theorem aux_11 : (x:Z)`x < 2` -> `x <= 1`.
Theorem aux_12 : (x,y,z:Z)`x<=y` ->`x-z<=y-z`.
Theorem aux_13 : (p, p1,p2, d, n:nat)
(`p1+2*n <= p2`\/`p2+n <= p1`) ->
((le (plus p1 d) p)
/\(lt p (plus (plus p1 d) d))) ->
~((le (plus p1 (mult (2) d)) p)
/\(lt (plus p1 (mult (2) n)) p)
\/(le (plus p2 d) p)/\(lt p (plus p2 n))).
Theorem lt1_le0 : (x:Z)`x<1`->`x<=0`.
Theorem pow_positive' : (x:nat)`0 <= (pow beta x)`.
Theorem pow_h_ge_pow_l : (x:nat)
`(pow beta (div2' x)) <= (pow beta (minus x (div2' x)))`.
Global Variable x: nat ref.
Definition bool2nat : bool -> nat :=
[b:bool]Cases b of true => (S O) | false => O end.
Definition bool2Z : bool -> Z :=
[b:bool]Cases b of true => (POS xH) | false => ZERO end.
Theorem Zmultbool_to_Zmult : (b:bool)(x:Z)(Zmultbool b x)=`(bool2Z b)*x`.
Definition Z2bool : Z -> bool :=
[z:Z]Cases z of ZERO => false | _ => true end.