handler leq {

    class java.lang.Integer;
    class IntUtil;


    constraint leq(java.lang.Integer, java.lang.Integer);


    rules {

        variable java.lang.Integer X, Y, Z;


        // ground @ leq(X, Y) <=> ground(X), ground(Y) I X=<Y.
        if(IntUtil.ground(X) && IntUtil.ground(Y)) {
            leq(X, Y)
        } <=> {
            IntUtil.le(X, Y)
        } ground;


        // reflexivity @ leq(X, X) <=> true.
        {
            leq(X, X)
        } <=> {
            true
        } reflexivity;


        // antisymmetry @ leq(X, Y), leq(Y, X) <=> X=Y.
        {
            leq(X, Y) && leq(Y, X)
        } <=> {
            X = Y
        } antisymmetry;


        // idempotence @ leq(X, Y) \ leq(X, Y) <=> true.
        {
            leq(X, Y) &\& leq(X, Y)
        } <=> {
            true
        } idempotence;


        // transitivity @ leq(X, Y), leq(Y, Z) ==> leq(X, Z).
        {
            leq(X, Y) && leq(Y, Z)
        } ==> {
            leq(X, Z)
        } transitivity;

    }//end of rules


    goal leq_Y_X_X_Y_Y_X {
        variable java.lang.Integer X, Y;
        leq(Y, X) && leq(X, Y) && leq(Y, X)
    }//end of leq_Y_X_X_Y_Y_X


    goal leq_X_Y_Z_X_Y_Z {
        variable java.lang.Integer X, Y, Z;
        leq(X, Y) && leq(Z, X) && leq(Y, Z)
    }//end of leq_X_Y_Z_X_Y_Z

}//end of handler leq