So, for now you are only verifying these two assignments: "m:=a; n:=b", right?{a > 0 ∧ b ≥ 0}

m := a; n := b

{Invariant: gcd(m,n) = gcd(a,b) ∧ n ≥ 0 }

Proof:

Pre -> [m:=a; n:=b]Invariant

[m:=a;n:=b][Invariant]

[m:=a; n:=b]{gcd(m,n) = gcd(m,n) ∧ b ≥ 0 }

So to prove:

{a > 0 ∧ b ≥ 0} -> {gcd(m,n) = gcd(m,n) ∧ b ≥ 0 }

I am not sure I understand everything you wrote. I am not familiar with the notation "Pre -> [m:=a; n:=b]Invariant". The way I learned it, a triple has the form {P}program{Q} where "program" is written without square brackets. I am also not sure this makes sense:

because it is neither a formula (because of braces) nor a triple.{a > 0 ∧ b ≥ 0} -> {gcd(m,n) = gcd(m,n) ∧ b ≥ 0 }

More importantly, to prove this fragment, I believe one needs to use the rules for compound statement (semicolon), assignment, and the rule of consequence. I am not sure where you use them.