%
\label{prop:em-eliminable}
Both uses of \texttt{Classical.em} in TauLib
are applied to decidable predicates
and can be replaced by decidable case analysis
(\texttt{Decidable.em} or the \texttt{by\_cases} tactic
with an explicit \texttt{Decidable} instance)
without changing any theorem statement or proof structure.
After replacement, the \texttt{Coordinates/Primes} module
reclassifies from \textbf{Cl}~(classical) to
\textbf{C}~(fully constructive).

In both cases, the predicate $P$ appearing in
\texttt{Classical.em $P$} has a \texttt{Decidable} instance:
\begin{itemize}
    \item Site~1: $P \equiv \forall\, d : \texttt{TauIdx},\;
          d \mid n \to d = 1 \lor d = n$.
          At each tower stage, \texttt{TauIdx} is \texttt{Fin}~$M_k$
          for some primorial $M_k$.
          Divisibility on \texttt{Fin}~$n$
          is decidable (reduce to \texttt{Nat.decidable\_dvd}).
          Equality on \texttt{Fin}~$n$ is decidable.
          The disjunction and implication of decidable propositions
          are decidable.
          The universal quantifier over a finite type
          of decidable propositions is decidable.
    \item Site~2: $P \equiv p \mid a$
          where $p, a : \mathbb{N}$.
          \texttt{Nat.decidable\_dvd} provides the instance directly.
\end{itemize}
In each case, replacing
\texttt{rcases Classical.em $P$ with h $|$ h}
by
\texttt{rcases Decidable.em $P$ with h $|$ h}
produces an identical proof term
except that the axiom dependency on
\texttt{Classical.em} is removed.
The resulting module passes
\texttt{\#print axioms} with no classical axioms.