Require Export sqrt_prog.
Require Export Decidable.
Lemma A1' : (X0:bool)(sp0,np0,nn0:nat)(m1,m2:(array bound modZ))
`(I m1 (plus np0 (mult (S (S O)) (div2' nn0))) (minus nn0 (div2' nn0)))
<(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0)))`
->`(I m2 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))
= (Zmultbool X0 (pow beta (minus nn0 (div2' nn0))))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))-
(I m1 (plus sp0 (div2' nn0))
(minus nn0 (div2' nn0)))`->X0=true.
Lemma l1
: (q:Z)
`0 <= q <= 2`->`(shift_2 q)*beta+(aux_shift_1 q) = q*beta'`.
Lemma suppress_1 : (n:Z)`1*n = n`.
Lemma Zmult_reg_r
: (A,B,C:Z)`A = B`->`A*C = B*C`.
Lemma l2 : (q:Z)`0 <= q <= 2`->`q*beta=(shift_2 q)*2*beta+2*(aux_shift_1 q)`.
Lemma l3 : (q:Z)(rb0:bool)(l:nat)(`q = 0`\/`q = 1`) ->(lt O l)->
`(q+(bool2Z rb0))*(pow beta l) = (shift_2 (q+(bool2Z rb0)))*
(pow beta l)*2+(pow beta (pred l))*(aux_shift_1 (q+(bool2Z rb0)))*
2`.
Lemma l4 : (nn,l:nat)(le l nn)->l=(minus nn (minus nn l)).
Lemma l5 : (f:Z)(l:nat)(`0<=f`)->`0<=f*(pow beta l)`.
Lemma l6 : (q:Z)(rb0:bool)`q = 0`\/`q = 1`->
`0<=(shift_2 (q+(bool2Z rb0)))`.
Lemma l7 : (A,B:Z)(`0<=A`)->(`0<=B`)->(`A<B`)->(`A<2*B`).
Lemma l8 :
(m2:(array bound modZ))(sp,l:nat)
(Zlt (Zmult `2` (I m2 sp (S l))) (pow beta (S l)))->
(Zlt (Zmult `2` (I m2 (S sp) l)) (pow beta l)).
Lemma l9 :
(m2:(array bound modZ))(sp,l:nat) (lt O l)->
(Zlt (Zmult `2` (I m2 sp l)) (pow beta l))->
`2*(I m2 (plus sp (pred l)) (S O)) < beta`.
Lemma l10 :
(m1,m2:(array bound modZ))(sp,l:nat)(c0:Z)(Hlt:(lt O l))(Hc0:`0<=c0`)
(`(I m1 sp l) = 2*(I m2 sp l)+c0 `)->
`(I m2 (plus sp (pred l)) (S O)) < beta'`.
Lemma l11 : (y:modZ)`0<=(modZtoZ y)`.
Lemma l12 : (p,sp,l:nat)(lt O l)->(le (plus sp l) p)->`(plus sp (pred l))<p`.
Lemma l14 :(m1:(array bound modZ))(sp:nat)
`(modZtoZ (isEvenOrOdd m1 sp)) = 0`
\/`(modZtoZ (isEvenOrOdd m1 sp)) = 1`.
Lemma l15 : (a,b:Z)`0<=a`->`0<=b`->`0<=a+b`.
Lemma l16 : (a,b,c,d:Z)`a<=c`->`b<d`->`a+b<c+d`.
Lemma l17 : (q:Z)(rb:bool)
(`q = 0`\/`q = 1`)->`0 <= (shift_2 (q+(bool2Z rb))) <= 1`.
Lemma v12 : (nn,l,sp,p:nat)(lt (1) nn)->(l=(div2' nn))->
~((le sp p)/\(lt p (plus sp l)))->
`p<>(plus sp (pred l))`.