Ok, je viens de comprendre les problèmes dans ma rédaction, suite à une petite conversation avec blo yhg :
J’utilise maladroitement la variable $p$ dans mon raisonnement, qui est une variable muette mutifié avec le quantificateur $\exists$. Il faudrait définir une fonction $p : \mathbf N \to \mathbf N : y \mapsto p(y)$, où $p(y)$ est l’unique entier tel que $y \in [ \![ \tau(p(y)), \tau(p(y) + 1) [\! [$, afin de pouvoir la réutilisée ultérieurement.
Donc pour $y$ naturel, s’il existe un couple $(n, k)$ de $\mathbf N^2$ tel que $y = f(n, k)$, alors $y \in [ \![ \tau(n + k), \tau(n + k + 1) [\! [$, ce qui permet d’écrire $n + k = p(y)$.
Ici, on a redéfini p seulement en fonction de y (selon l’encadrement) et non pas de n + k, ce qui permet d’exprimer les deux entiers $n$ et $k$ en fonction de $y$ (bon ici, je fais volontairement l’impasse sur des calculs qui ont déjà été effectués précédemment dans le topic).
On vérifie assez aisément, à l’aide de l’encadrement de y, que ce sont deux naturels.
On peut ainsi conclure que $f$ est inversible à gauche et à droite via l’application qui envoi sur $y$ le couple $(n(y), g(y))$.
J’en suis venu à la conclusion qu’une preuve algébrique n’est pas vraiment judicieuse. Parce que montrer que N et N² sont équipotent ne nécessite pas obligatoirement de connaître la bijection, mais simplement de la mettre en évidence.
Et à vrai dire, il est possible de la mettre en évidence via une interprétation géométrique, c’est plus joli et simple je trouve.
Quand à ma rédaction, elle n’est vraiment pas claire je le conçois.
Je m’excuse pour le spam et tout, je sais que le topic tend bien trop inutilement en longueur.
Je pense que je vois les choses de manière trop complexe, du coup je m’embrouille l’esprit et je raisonne faux. J’ai besoin d’être plus concis, moins long, plus simple.