扩展欧几里得算法的非递归实现的证明算法

在阅读《密码学与网络安全》遇到扩展的欧几里得算法，一直不太明白它的非递归算法（迭代）的有效性在哪里。
于是就去网上看一些证明，递归算法的证明蛮多，而且都比较好懂。非递归算法的证明倒是很少。
参考至 http://blog.csdn.NET/yoer77/article/details/69568676
这个博客非常齐全，但是非递归的证明我还是看了两三个小时才看懂，因此就结合自己的理解，自己写了一份个人认为比较清晰的证明：
解 s * a + t * b = gcd(a,b)
初始化： r1 = a , r2 = b , s1 = 1, s2 = 0, t1 = 0, t2 = 1.
循环过程：

while(r2 > 0) { q = r1 / r2; r = r1 - q * r2; //也就是r = r1%r2; r1 = r2; r2 = r; s = s1 - q * s2; s1 = s2; s2 = s; t = t1 - q * t2; t1 = t2; t2 = t; } gcd(a,b) = r1; s = s1; t = t1;

【扩展欧几里得算法的非递归实现的证明】附上自己手写证明过程的扫描版：