/* program computing a divisor for factorisation, by Bressoud */

int fermat(int N, int R)
pre(  N >= 1  &&   (R-1) ^2 < N   &&   N <= R^2  &&  N%2 == 1  );
    {
    int u,v,r;
    

    u=2*R+1;
    v=1;
    r=R*R-N;

    inv(   4*(N + r) == u^2 - v^2 - 2*u + 2*v   &&   v%2 == 1   &&   u%2 == 1   &&   N >= 1  );
    while (r!=0)
        {
        if (r>0) 
            {
            r=r-v;
            v=v+2;
            }
        else
            {
            r=r+u;
            u=u+2;
            }
        }

    assert(u!=v);
    return((u-v)/2);
    }
post(N % result==0);