Require Export specifications.
Theorem betaGt0 : `0 < beta `.
Theorem betaGt2 : `2 < beta `.
Theorem I_positive : (l,n:nat)(a:(array bound modZ))
(Zle ZERO (I a n l)).
Hints Resolve I_positive.
Lemma Zle_mult_2
: (a,b,c:Z)`0 < a `->`b <= c`->`a*b <= a*c`.
Lemma Impnumber_bound
: (m:(array bound modZ); l,pos:nat) `(I m pos l) < (pow beta l)`.
Lemma Impnumber_decompose : (m:(array bound modZ);h:nat;l:nat;np:nat)
`(I m np l)+(pow beta l)*(I m (plus np l) h)
=(I m np (plus l h))`.
Theorem Impnumber_unchanged : (a,l:nat)(m1,m2:(array bound modZ))
((p:nat)(le a p)/\ (lt p (plus a l)) -> (access m1 p)=(access m2 p))->
(I m1 a l)=(I m2 a l).
Lemma Impnumber_access : (a:nat)(m:(array bound modZ))
(I m a (S O))=(modZtoZ (access m a)).
Lemma pow_positive : (n:nat)(Zlt O (pow beta n)).
Lemma borrow_positive :
(a,b,c,d,e:Z)`0<d`->`0<=a<d`->`0<=b<d`->`0<=c` ->`a=b-c+e*d`->`0<=e`.
Lemma borrow_positive' :
(a,b,c,d,e:Z)`a=e*d+b-c`->`0<d`->`0<=a<d`->`0<=b<d`->`0<=c` ->`0<=e`.
Lemma borrow_bound :
(a,b,c,d,e:Z)`a=e*d+b-c`->`0<d`->`a<d`->`0<=b`->`c<=d` ->`e <= 1`.
Lemma Impnumber_between : (m:(array bound modZ))(pos, l:nat)
`0 <= (I m pos l) < (pow beta l)`.
Theorem Impnumber_unchanged_bis :
(a,l:nat)`0<=a`/\`(plus a l) <=bound`->(m1,m2:(array bound modZ))
((p:nat)`0<=p<bound`/\(le a p)/\ (lt p (plus a l)) -> (access m1 p)=(access m2 p))->
(I m1 a l)=(I m2 a l).