None
Conclusion:
n:. GCD([a];[b];n) [a] > 0 [b] > 0 {#GCD#} [a] = n
1. GCD([a];[b];n) [a] > 0 [b] > 0 {#GCD#} [a] = n
n:
. GCD([a];[b];n) 
[a] > 0 [b] > 0 {#GCD#} [a] = n n:. GCD([a];[b];n) [a] > 0 [b] > 0 {#GCD#} [a] = n
n
] THENM
InstLemma `hoare_gcd_2` [] THENA Auto [a] > 0 [b] > 0 {#GCD#} [a] = n