Caractérisation du pgcd

@YvesM : Très franchement, ce genre d'écriture est lisible.

@jp59 : Bah on applique le "quel que soit $a$" de l'hypothèse de récurrence à l'entier $b$, aucun problème.

Tu n'as pas vu mon message ?

@jp59, à noter que le pgcd de $a$ et $b$ est par définition la borne inférieure de $\{a, b\}$ pour la relation de divisibilité. Or dans n'importe que ensemble ordonné, dire que c est la borne inférieure de $a$ et $b$, c'est trivialement équivalent à dire que $\{ x \leqslant a \} \cap \{ x \leqslant b \} = \{ x \leqslant c \}$.

P.S. Non AD ! prière de ne pas faire des correction intempestives ! Merci.

Ce que certains appellent "récurrence complète":
Si H(0) est vrai
Si (quel que soit r<b, H(r)) implique H(b)
Alors H(b) est vrai pour tout entier naturel b.

Cordialement.

Bien sûr !

Mais la preuve donnée par Jp59 le fait. Je suis resté dans son cadre. Et comme je n'ai regardé que l'aspect logique, je n'ai pas regardé si on pouvait la faire fonctionner en supprimant le paragraphe "supposons b=0" et en commençant le suivant par "soit $b \in \mathbb N$.
D'ailleurs, quid de "la division euclidienne de a par b" quand b est nul ?

Donc le "pas besoin de l'hypothèse sur 0" n'est vrai que si la preuve générale traite aussi le cas 0.

Cordialement.

Non, si on peut bien prouver la propriété $\forall n\in\mathbb N\ (\forall p\in [1..n]\ P(p)\ ) \Rightarrow P(n)$; car cette propriété est automatiquement vraie pour n=0 (il n'y a pas de p<n).

Cordialement.