Sequent calculus: $0<1$ Considering the axioms of real closed ordered fields, I'm having trouble proving $0<1$ using Gentzen sequent calculus enriched with the cut rule, i.e, $$\text{Ax}_{\text{RCOF}}\vdash 0<1.$$
Using the trichotomy axiom I was able to obtain the following sequents $$0<1,..., R\rightarrow 0<1$$
$$1<0,..., R\rightarrow 0<1$$
$$0\cong 1,..., R\rightarrow 0<1,$$ where $R$ is some subset of the set of axioms of RCOF and "$...$" are consequences of applying the rules $L\forall$ and $L\vee$. Now, the first sequent is an axiom and. Knowing that $\neg\, 0\cong 1$ belongs to $R$, I apply the rule $L\neg$ to it and I derive the third sequent.
My question: I've tried a couple different approaches but wasn't able to derive the second. Any suggestions? Many thanks in advance.
 A: Wou have Trichotomy: exactly one of $1 < 0$ or $1=0$ or $0 < 1$ holds.
If we use the Law of Order: if $1 < 0$ and $z > 0$, then $1z <0z$, we have $z < 0$, contradicting Trichotomy.
Thus, we have $\lnot (1 < 0)$.
And we have the Non-triviality axiom: $\lnot (1=0)$.
In terms of sequents, we have:

$\text {Ax} \to \lnot (1=0)$, and


$\text {Ax} \to \lnot (1 < 0)$.

Here is the derivation:

*

*$(1 < 0) \to (1 < 0)$


*$[(1=0) \lor (0 < 1)] \to [(1=0) \lor (0 < 1)]$


*$(1 < 0) \lor [(1=0) \lor (0 < 1)] \to (1 < 0), [(1=0) \lor (0 < 1)]$ --- from 1) and 2) by $(\lor \text L)$, that is:



*$\text {Ax}\to (1 < 0), [(1=0) \lor (0 < 1)]$



*$\text {Ax} \to \lnot (1 < 0)$ --- see above


*$\text {Ax}, (1 < 0) \to$
The next step is to apply Cut to 3) and 5):


*$\text {Ax} \to (1=0) \lor (0 < 1)$.

Now repeat:


*$(1=0) \to (1=0)$


*$(0<1) \to (0<1)$


*$(1=0) \lor (0<1) \to (1=0),(0<1)$
Cut on 6) and 9):


*$\text {Ax},\to (1=0),(0<1)$.


*$\text {Ax}, \lnot (1=0) \to (0<1)$


*$\text {Ax} \to \lnot (1=0)$ --- see above



*$\text {Ax} \to (0<1)$ --- from 11) and 12) by Cut.


