Proving properties of simple power function in Dafny

The following verifies fine and for obvious reasons.

function power(x: int, y: int) : int
    requires y >= 0
    ensures y == 0 ==> power(x,y) == 1
    ensures y > 0 && y % 2 == 0 ==> power(x,y) == power(x*x,y/2)
    ensures y > 0 && y % 2 == 1 ==> power(x,y) == x * power(x*x,(y-1)/2)
    decreases y
{
    if y == 0 then
        1
    else if y % 2 == 0 then
        power(x*x, y/2)
    else 
        (x * power(x*x,(y-1)/2))
}

I wish to verify the following two properties as well by addding corresponding ensures clauses --

ensures y > 0 ==> power(x, y) == x * power(x, y - 1)
ensures forall a :: 0 <= a <= y ==> power(x, y) == power(x, a) * power(x, y - a)

Adding either one of the above ensures clauses takes dafny verify test.dfy into a seemingly unending loop with CPU pegged at 100%. How do I verify those properties of this function?

Should I add lemmas that prove those properties step by step?

A problem that will often come up is that multiplication is not decidable and frequently it will cause Dafny/Z3 to not verify unless you force it to think symbolically which you can do by making the operations opaque. To verify properties about functions in Dafny induction is the name of the game.

module SO4 {
opaque function prod(x: int, y: int): int {
    x * y
}

lemma ProdAssoc(x: int, y: int, z: int)
    ensures prod(x, prod(y,z)) == prod(prod(x, y), z)
{
    reveal prod();
}

opaque function div(x: int, y: int): int 
    requires y != 0
{
    x / y
}

function power(x: int, y: int) : int
    requires y >= 0
    decreases y
{
    reveal prod();
    reveal div();
    if y == 0 then
        1
    else if y % 2 == 0 then
        power(prod(x,x), div(y,2))
    else 
        prod(x, power(prod(x,x), div(y-1,2)))
}

lemma PowerResults(x: int, y: int) 
    ensures y == 0 ==> power(x,y) == 1
    ensures y > 0 && y % 2 == 0 ==> div(y,2) >=0 && power(x,y) == power(prod(x,x), div(y,2))
    ensures y > 0 && y % 2 == 1 ==> div(y-1,2) >=0 && power(x,y) == prod(x, power(prod(x,x),div(y-1,2)))
{
    reveal div();
    reveal prod();
}
lemma PowerOne(x: int)
    ensures power(x, 1) == x
{
    reveal div();
    reveal prod();
    assert div(0,2) == 0;
    calc {
        power(x, 1);
        {PowerResults(x, 1);}
        prod(x, power(prod(x,x), div(1-1, 2)));
        prod(x, 1);
        x;
    }
}

lemma  PowerCompleteness(x: int, y: int)
    requires y > 0
    ensures power(x, y) == prod(x , power(x, y - 1))
    decreases y
{
    PowerResults(x,y);
    if y == 1 {
        assert div(y-1,2) == 0 by {
            reveal div();
        }
        calc { 
            power(x,y);
            prod(x, power(prod(x,x),div(y-1,2)));
            prod(x,1);
            {reveal prod();}
            x;
            {reveal prod();}
            prod(x , 1);
            prod(x , power(x, y-1));
        }
        

    }else if y == 2 {
        assert div(y,2) == 1 by {
            reveal div();
        }
        assert div(1-1, 2) == 0 by {
            reveal div();
        }
        calc {
            power(x,y);
            power(prod(x,x), 1);
            {PowerResults(prod(x,x), 1);}
            prod(prod(x,x), power(prod(prod(x,x), prod(x,x)), 0));
            prod(prod(x,x),1);
            {reveal prod();}
            prod(x,x);
            {PowerOne(x);}
            prod(x,power(x, y-1));
        }
    }else{
        if y % 2 == 0 {
            assert y-2 > 0;
            assert (y-2)%2 == 0;
            assert 0 < div(y,2) < y by {
                reveal div();
            }
            calc {
                div(y-2,2);
                {reveal div();}
                div(y,2)-1;
            }
            calc {
                prod(x,power(x,y-1));
                {PowerCompleteness(x, y-1);}
                prod(x,prod(x,power(x, y-2)));
                {ProdAssoc(x,x, power(x, y-2));}
                prod(prod(x,x),power(x, y-2));
                {PowerResults(x, y-2);}
                prod(prod(x,x),power(prod(x,x), div(y-2,2)));
                prod(prod(x,x),power(prod(x,x), div(y,2)-1));
                {PowerCompleteness(prod(x,x), div(y,2));}
                power(prod(x,x), div(y,2));
                power(x,y);
            }

        }else{
            assert y >= 3;
            assert div(y-3,2) >=0 by {
                reveal div();
            }
            assert (y-1)%2==0;
            assert (y-2)%2==1;
            calc {
                div(y-1,2) -1;
                {reveal div();}
                div(y-3,2);
            }
            assert 0 < div(y-1,2) < y  by { 
                 reveal div();
            }
            PowerCompleteness(x, y-1);
            PowerCompleteness(prod(x,x), div(y-1,2));
            calc {
                power(x,y);
                prod(x, power(prod(x,x), div(y-1,2)));
                prod(x,prod(prod(x,x),power(prod(x,x), div(y-3,2))));
                prod(x , prod(x , power(x,y-2)));
                prod(x , power(x, y-1));
            }

        }

    }
}

    method Test() {
        assert power(2, 37) == 137438953472 by {
            reveal prod();
            reveal div();
        }
    }

}