Dealing with trichotomy laws in arguments requires the Proof by Contradiction methodoloy? I recently carried out a proof that required me to invoke the law of trichotomy on $\mathbb R$ in order to progress my argument. I found that two of the three cases led to contradictions, so I casually concluded the 3rd option must be the valid case. After completing my overall argument, I mulled over whether this aforementioned step was actually an instance of applying two "mini" versions of a proof by contradiction.
Here are my thoughts:

Firstly, I assume that the notion of proof by contradiction written in the form of sequent calculus in the context of classical logic, where Law of Excluded Middle is in effect, can be written as:
$$
\begin{array}{c}
\neg A &\vdash \bot \\
\hline
&\vdash A
\end{array}
\quad\quad(\dagger)$$
If this is correct, then I'd like to generalize my description from my first paragraph as:
$$\Gamma \vdash (P \land \neg Q \land \neg R) \lor(\neg P \land Q \land \neg R)\lor(\neg P\land \neg Q \land R)$$, where the disjunction on the right side is capturing the logical features of the trichotomy rule. (For the sake of argument, let's say that $R$ was the formula that I ultimately proved must be the true one)
Next, I believe I carried out these two steps:
1A)
\begin{array}{c}
\Gamma, P \land \neg Q \land \neg R  &\vdash \bot \\
\end{array}
1B)
\begin{array}{c}
\Gamma, \neg P \land Q \land \neg R  &\vdash \bot \\
\end{array}
Applying $(\dagger)$ to each of these sequents, I get:
2A) $\vdash \neg \Gamma \lor (\neg P \lor Q \lor R) $
2B) $\vdash \neg \Gamma \lor ( P \lor \neg Q \lor R) $
At this point, when I assume $\Gamma$, I effectively conclude:
$\Gamma \vdash (\neg P \lor Q \lor R) \land ( P \lor \neg Q \lor R)$, which means $\Gamma \vdash R$ because $[[(P∧¬Q∧¬R)∨(¬P∧Q∧¬R)∨(¬P∧¬Q∧R)]∧[(¬P∨Q∨R)∧(P∨¬Q∨R)]]→R$ is a tautology.
Is this essentially correct? If so, then I clearly employed the method of proof by contradiction, yes?

I raise this point because I have seen people ask questions of the form: "I want to prove this statement constructively and not use proof by contradiction". In the proof that I previously alluded to, I carried out what I originally thought was a constructive proof. This "constructive" proof contained, as one of its subarguments, the previously described methodology of handling the different cases posed by the trichotomy rule. Given this, I subsequently wondered if my proof would qualify as constructive.

Edit: In retrospect, it seems that my $\dagger$ would have been more appropriately encoded as:
$$
\begin{array}{c}
A &\vdash \bot \\
\hline
&\vdash \neg A
\end{array}
\quad\quad(\dagger)$$
, which is an instance of $(\rightarrow I)$, and therefore, this overall approach made no use of the excluded middle (nor a proof by contradiction). Instead, this was a proof by negation
 A: "Proof by contradiction" is ambiguous from a constructive point of view.
We have Trichotomy:

$x=a ∨ x<a ∨ x>a$,

whose logical form is: $P \lor Q \lor R$.
The structure of the proof is to show that if two of the cases do not hold, then necessarily the third will do. In formula:

$\Gamma, (P \lor Q \lor R), ¬P,¬Q \vdash R$.

Working with Natural Deduction, we have two nested Disjunction Elim: $P \lor (Q \lor R)$.
Assuming the first disjunct with $\lnot P$ we derive $\bot$ and thus $R$. The same with $\lnot Q$.
The last case obviously implies $R$.
Thus, we can close the two nested sub-proofs to conclude with $R$.

In conclusion, we need Ex falso: $(\bot \text E) \ \ \bot \vdash \varphi$ but not DNE: $"\text {if } \lnot \varphi \vdash \bot, \text { then } \vdash \varphi"$, which is equivalent to LEM.
From a constructive point of view, the rule: $"\text {if } \varphi \vdash \bot, \text { then } \vdash \lnot \varphi"$ is simply $(\to \text I)$, and does not imply DNE.


As per Daniel's comment above, one thing is to prove trichotomy, and another is to use it.
