Correct proof for Hoare Triple - formal proof

Question

I'm working on a Hoare logic proof of the following while loop: Here is the loop and what I have so far:

All variables are integers.
{true}
i := n;
while i>0 loop
    i := i - 1
end loop
{i = 0}

And here is my attempt at a proof:

1. {i-1=0} i:=i-1 {i=0} (Assignment rule)
2. i>0 ∧ i-1 >= 0 -> i > 0 (Side condition)
3. {i>0 ∧ i-1 >= 0} i:=i-1 {i=0} (Rule i strengthen precondition from lines 2,1)
4. {i>0} (loop rule using line 3)
   while i>0 loop i:=i-1 end loop
   {i>0 ∧ ¬(i>0) -> i=0} 
5. i>0 ∧ ¬(i>0) -> i=0 (Side condition)
6. {i>0} while i>0 loop i:= i-1 end loop {i=0} Rule e weaken postcondition (5,6)

I'm not sure that my work is correct.

Here is a completed example of a Hoare proof:

    {x > 0}
     i := j^2
     n := sqrt(i)
    {n > 0}

    1. { √i > 0} n:=√i {n > 0} (Assignment rule)
    2. i > 0 →  √i > 0 [Side condition]
    3. {j^2 > 0} i:=j^2 {i > 0} (Assignment rule)
    4. {j^2 > 0} i:=j^2 {√i > 0} (e)2,3 (weaken post condition using lines 2 and 3)
    5. {j^2 > 0} i:=j^2 ; n:=√i {n > 0} (Compound statement rule using line 4 and 1)
    6. j > 0 → j^2 > 0 [Side condition]
    7. {j > 0} i:=j^2 ; n:=√i {n > 0} (i)6,5 (strengthen precondition using lines 6 and 5)