diff --git a/fonction récursive primitive.md b/fonction récursive primitive.md
index e3e3e7a3..e08a56af 100644
--- a/fonction récursive primitive.md	
+++ b/fonction récursive primitive.md	
@@ -34,7 +34,7 @@ source:
 >  - $E$ contient la fonction successeur $S$
 >  - $E$ est clos par composition, c'est-à-dire que si $n,p \in \mathbb{N}$ , si $f_1, f_2, \dots, f_{n}$ sont des fonctions de $\mathscr{F}_{p}$ qui sont aussi dans $E$, et si $g \in \mathscr{F}_{n}$ est aussi dans $E$, alors la fonction composée $g(f_1, f_2, \dots, f_{n})$ appartient à E
 >      - i on accepte l'abus de notation $g(f_1, f_2, \dots, f_{n})$ pour la composition
->  - $E$ est clos par récurrence, cc'est-à-dire que si $p \in N$, si $g \in \mathscr{F}_{p}$ et $h \in \mathscr{F}_{p+2}$ sont dans $E$, alors la fonction $f \in \mathscr{F}_{p+1}$ définie par récurrence à partir de $g$ et $h$ est aussi dans $E$ : $f : \begin{cases} f(x_1,x_2, \dots, x_{p}, 0) = g(x_1, x_2, \dots, x_{p})\\ f(x_1, x_2, \dots, x_{p}, y+1) = h(x_1, x_2, \dots, x_{p}, y, f(x_1, x_2, \dots, x_{p}, y)) \end{cases}$
+>  - $E$ est clos par récurrence, cc'est-à-dire que si $p \in \mathbb{N}$, si $g \in \mathscr{F}_{p}$ et $h \in \mathscr{F}_{p+2}$ sont dans $E$, alors la fonction $f \in \mathscr{F}_{p+1}$ définie par récurrence à partir de $g$ et $h$ est aussi dans $E$ : $f : \begin{cases} f(x_1,x_2, \dots, x_{p}, 0) = g(x_1, x_2, \dots, x_{p})\\ f(x_1, x_2, \dots, x_{p}, y+1) = h(x_1, x_2, \dots, x_{p}, y, f(x_1, x_2, \dots, x_{p}, y)) \end{cases}$
 >      - i on pourra noter $f = \rho(g, h)$
 > 
 ^definition
@@ -125,5 +125,21 @@ Dans cette section, on démontre que quelques fonctions élémentaires sont réc
 > > > Cela montre que cette fonction est bien récursive primitive
 > 
 > > [!démonstration]- Démonstration
+> > Notons $\operatorname{prec} = \lambda x.x \dot{-}1$. On a démontré dans le lemme précédent que cette fontion est récursive primitive.
+> > Maintenant, on peut définir $\operatorname{sub} = \lambda xy.x \dot{-} y$ comme :
+> > $\operatorname{sub} = \rho(P_1^{1}, \operatorname{prec}(P_3^{3}))$
+
+> [!proposition]+ La fonction signe est récursive primitive
+> On définit la [[fonction signe]] par :
+> $\operatorname{sg}: \begin{cases} \operatorname{sg}(0) = 0\\ \operatorname{sg(x) = 1 \text{ si } x \neq 0} \end{cases}$ (car on est sur $\mathbb{N}$)
+> Cette fonction est récursive primitive
+> > [!démonstration]- Démonstration
+> > On peut écrire $\operatorname{sg}$ de plusieurs manières :
+> >  - $\operatorname{sg} = 1 \dot{-} (1 \dot{-}x)$
+> >  - $\operatorname{sg} = \rho(C_0^{0}, C_2^{1})$
+> > Ce qui montre, dans tous les cas, que $\operatorname{sg}$ est récursive primitive
+
+> [!proposition]+ Le prédicat $x>y$ est récursif primitif
+> Le prédiat $x>y$ est récursif primitif (c'est-à-dire que l'ensemble $$)
 
 # Exemples