/* program computing a divisor for factorisation, by Knuth */
int fermat(int N, int R)
pre( N>=1 && (R-1)*(R-1) <N && N<=R*R && N%2==1 );
{
int u,v,r;
u=2*R+1;
v=1;
r=R*R-N;
inv( 4*(N+r)==u*u-v*v-2*u+2*v && v%2==1 && u%2==1 && N>=1 );
while ( r!=0 )
{
inv( 4*(N+r)==u*u-v*v-2*u+2*v && v%2==1 && u%2==1 && N>=1 );
while ( r>0 )
{
r=r-v;
v=v+2;
}
inv( 4*(N+r)==u*u-v*v-2*u+2*v && v%2==1 && u%2==1 && N>=1 );
while ( r<0 )
{
r=r+u;
u=u+2;
}
}
assert( u!=v );
return((u-v)/2);
}
post( N % result==0 );