Axiome ou pas axiome

Oui, la première peut être démontrée à partir de la seconde.
En fait, tu n'as pas besoin de formuler d'équivalence pour la première : "Si a<c, alors a+b < c+b " suffit. Ça exprime la compatibilité de l'ordre avec l'addition.

Bof bof.
Comme je l'ai déjà dit, formuler une équivalence est inutile. ""Si a <= c, alors a+b <= c+b " suffit.
Et pour la multiplication, outre les coquilles qui consistent à écrire deux fois a au lieu de a et b, il suffit d'avoir "Si 0 <= a et 0 <= b, alors 0 <= ab". Les autres sont conséquences de ça.

$a<b\Leftrightarrow 0<b-a$
donne des calculs plus simples que
$a<b\Leftrightarrow a-b<0$
car les positifs sont stables par multiplication

Tout se mélange (je veux dire dans les échanges...).
Je trouve que la première propriété posée devrait être la compatibilité de l’ordre avec l’addition.
Puis la même chose avec la multiplication (par un nombre positif).

Je préférerais dans un premier temps n’utiliser que le symbole $\leq$ (je veux dire toujours dans le même sens).
Ça fait échanger les membres quand, par exemple, on passe à une fonction décroissante (inverse de positifs, opposé, ...).

Avec ça on démontre plein de choses, notamment l’ordre sur les carrés, les racines carrées, les inverses...
Plus simple : ajout membre à membre, multiplication (positive) membre à membre.

C'est la définition de la compatibilité de la structure de groupe avec un ordre, ce qui permet de parler de groupe ordonné. Mais ce n'est pas le sujet.
Que ça soit d'un point de vue intuitif ou de la définition via les axiomes de Peano, la définition de $x\leq y$ est $\exists a\geq 0 y=a+x$. On démontre toujours dans Peano la compatibilité de l'annélide $(\mathbb{N},+,\cdot )$ avec l'ordre. Puis on constate la conservation de cette compatibilité en remontant à $\mathbb{R}$ via les procédés attendus: symétrisation, corps des fractions et "complétudition" (cette dernière repose d'ailleurs autant sur une méthode liée à l'ordre qu'à l'algèbre et pardon pour le néologisme). À chaque étape, il faut bien sûr redéfinir ce qu'est l'ordre, mais la recette est automatique et le nouvel ordre est systématiquement compatible avec l'ancien (exemple pour le passage de $\mathbb{Z}$ au corps des fractions: l'ordre induit $(a,b)\leq (x,y) \leftrightarrow ay\leq bx$ est compatible avec la relation d'équivalence $(a,b) .E. (x,y) \leftrightarrow ay= bx$ et on voit bien ce que ça donne avec $b=y=1$ pour retourner sur $\mathbb{Z}$).
Bref, de base, la définition ("axiomatiquement intuitée", ou démontrée dans Peano), c'est plutôt $a\leq b \leftrightarrow 0 \leq b-a$, mais on prend plutôt l'autre relation dans la formulation de la définition d'un groupe ordonnée, c'est équivalent (dans un groupe), mais ça permet de ne pas "rentrer dans le dur" dés la définition en y ajoutant la définition de ce qu'est un "élément positif".

Je ne fais pas de cours de seconde.
Mais ce que je sais, c'est que pour axiomatiser la notion de corps ordonné, on peut au choix :
- avoir une relation d'ordre total, demander la compatibilité avec l'addition $a\leq b \implies a+c\leq b+c$ et la multiplication $(0\leq a\text{ et }0\leq b)\implies 0\leq ab$,
- ou avoir le sous-ensemble $P$ des éléments positifs ou nuls, auquel on demande d'être stable par addition et multiplication, que $P\cup -P$ soit le corps tout entier , et que $-1\not\in P$.
Le lien entre les deux est bien sûr $x\leq y \Leftrightarrow y-x \in P$.