Cette preuve modélise le partage par soustractions successives.
Considérons l'algorithme suivant pour \(\textcolor{olive}{a}\in\mathbb{N}\) et \(\textcolor{colordef}{b}\in\mathbb{N}^*\) :
- Initialisation : Poser \(\textcolor{orange}{r}=\textcolor{olive}{a}\) et \(\textcolor{colorprop}{q}=0\).
- Boucle : Tant que \(\textcolor{orange}{r}\ge \textcolor{colordef}{b}\) faire : $$ \textcolor{orange}{r}\leftarrow \textcolor{orange}{r}-\textcolor{colordef}{b} \quad\text{et}\quad \textcolor{colorprop}{q}\leftarrow \textcolor{colorprop}{q}+1. $$
Terminaison : Comme \(\textcolor{colordef}{b}>0\), la valeur de \(\textcolor{orange}{r}\) décroît à chaque étape et reste positive ou nulle. Elle finit donc par satisfaire \(\textcolor{orange}{r}<\textcolor{colordef}{b}\) en un temps fini.
Invariant : La relation \(\textcolor{olive}{a}=\textcolor{colordef}{b}\textcolor{colorprop}{q}+\textcolor{orange}{r}\) est conservée à chaque itération. À l'arrêt, on a bien \(0\le \textcolor{orange}{r}<\textcolor{colordef}{b}\).
Unicité : Si \(\textcolor{olive}{a}=\textcolor{colordef}{b}q+r=\textcolor{colordef}{b}q'+r'\) avec \(0\le r,r'<\textcolor{colordef}{b}\), alors \(\textcolor{colordef}{b}(q-q')=r'-r\). Or \(-(\textcolor{colordef}{b}-1)\le r'-r\le \textcolor{colordef}{b}-1\), donc le seul multiple de \(\textcolor{colordef}{b}\) dans cet intervalle est \(0\). Ainsi \(r=r'\) et \(q=q'\).