algorithm - Loop invariant proof -

i running issue coming post-condition , showing partial correctness of piece of code.

{ m = ≥ 0 }   x:=0; odd:=1; sum:=1;   while sum<=m     x:=x+1; odd:=odd+2; sum:=sum+odd   end while { postcondition } 

i'm not looking answer, assignment school, insight , perhaps pointing in right direction. have constructed table of values, , cannot come loop invariant.

x   odd sum m   (x + 1)^2   odd - x (odd - x)^2 0   1   1   30    1            1        1 1   3   4   30    4            2        4 2   5   9   30    9            3        9 3   7   16  30    16           4        16 4   9   25  30    25           5        25 5   11  36  30    36           6        36  sum = (odd - x)^2 

i have outcome of loop perfect square following m, i'm not sure how write that.

as always, appreciated.

loop invariant is:

odd = 2x+1 sum = (x+1)^2 

proof:

induction base: trivial.

induction step:

new_x = x+1 new_odd = odd+2 = 2(x+1)+1 = 2*new_x+1 new_sum = sum+new_odd = (x+1)^2+2(x+1)+1 = new_x^2+2*new_x+1 = (new_x+1)^2