Proving the correctness of the following Hoare triple, $\{a[i] ≥ 0\} a[i] := a[i] + a[j] \{a[i] ≥ a[j]\}$

Question

How can I prove the correctness of the following Hoare triple, $\{a[i] ≥ 0\} a[i] := a[i] + a[j] \{a[i] ≥ a[j]\}$

Is it just enough to show $(a[i] + a[j] ≥ a[j] ∧ (i ≠ j))$ to prove it or do I have to show it leads to the precondition?

I think that I need consider all cases for i, j somehow.

Is this how I could do it?

$$\{a[i] > 0\} => \\ \{a[i] + a[j] ≥ a[j]\} \\ a[i] := a[i] + a[j] \\ \{a[i] ≥ a[j]\}$$

Answer 1

This is probably how I would write it (can't use latex b/c it is too wide):

              Logic                   
 -------------------------------      ------------------------------------------------------ Assignment
 a[i] ≥ 0 ⇒ a[i] + a[j] ≥ a[j]       {a[i] + a[j] ≥ a[j]} a[i] := a[i] + a[j] {a[i] ≥ a[j]}
 ------------------------------------------------------------------------------------------------Precondition Strengthening
            {a[i] ≥ 0} a[i] := a[i] + a[j] {a[i] ≥ a[j]}