Axomatic Semantic Proof System on while if-else statement

[animefun2]

I have diffcult proving by axiomatic semantic of a given program

by using the rules:
1. Rule of Sequence
2. Rule of Consequence
3. Rule of Assignment
4. Rule of Condition
5. Rule of iteration

{ x=m ^ y=n }
z := 1;
while y != 0 loop
       if y mod 2 = 0 then
             x := x * x;
             y := y / 2;
       else 
             z := z * x;
             x := x * x;
             y := ( y - 1 ) / 2;
       end if;
end loop;
{ z=m power n meaning m mutiply it self n times }

{ Hint: A good invariants to choose z . x power y  = m power n }

I have read book the Programming Languages by Robert W. Sebesta Eight Edition but the book about program proofs but there are only solutions of while and if-statements proof individually so i asked my professor he gave me a hint the i should work a little from the top then a little from the bottom till i will work my way in like using the postcondition of the assignment statement as precondition of the while statement xD i really i need help