Variant et Invariant

Voici un programme pour lequel je n'arrive pas à déterminer le variant et l'invariant:

def PGCD(a,b):
"""permet de déterminer le PGCD de deux nombres"""
R,r=a,b
while r! =0:
R,r=r,R%n
return R

Le variant du programme est la variable 'r'.
Si l'on note r_n sa n-ième valeur alors r_{n+1}<r_n et la suite strictement décroissante d'entiers est non minorée donc dépasse '0'.

L'invariant est a_n=pgcd(R_n,r_n)
a_{n+1}=pgcd(r_n,R_n%r_n) = pgcd(r_n, R_n-q r_n) = pgcd(r_n, R_n)=a_n car on peut faire une transvection sur les pgcd.