Fin de l'exemple

• Commençons par montrer que le programme s'arrête. La séquence formée par les valeurs de $r$ au fil des itérations est strictement décroissante. Il y a donc nécessairement un moment où la valeur de $r$ sera strictement inférieure à celle de $b$.
• Maintenant, nous pouvons terminer la preuve de validité :
  • Si le programme s'arrête, c'est que la condition du Tant que n'est plus satisfaite, donc que $r < b$.
  • Il reste à montrer que $r \geq 0$. Comme $r$ est diminué de $b$ à chaque itération, si $r < 0$, alors à l'itération précédente la valeur de $r$ était $r^\prime = r + b$, or $r^\prime = r + b < b$ car $r < 0$. Nous venons de montrer que si $r$ était strictement négatif, alors la boucle se serait arrêtée à l'itération précédente, ce qui est absurde. Donc nécessairement $r \geq 0$.

Résumons, le programme s'arrête avec $0 \leq r < b$ et la propriété $a = bq + r$ est vérifiée à chaque itération, ces deux propriétés nous démontrent que l'algorithme effectue bien la division de $a$ par $b$.