In classical logic, using the ZF axioms, one can show that there is an isomorphism between the Dedekind cuts in the rationals, and the equivalence classes of Cauchy sequences. One can also (without AC) choose a representative from each equivalence class of Cauchy sequences. (EDIT: In high school one might chose decimal fractions, and represent $\pi$ by the sequence $(3, 3.1, 3.14,\ldots)$; a more sophisticated approach might choose continued fractions and represent $\pi$ by the sequence $(3, 22/7, 333/106,\ldots)$.
The fundamental theorem of algebra (every non constant non-constant polynomial with real or complex coefficients has a zero in the complex numbers) can be proved without AC. In fact, there is a quite explicit algorithm that computes, for each irreducible polynomial (with leading coefficient 1, to be on the safe side), the roots of this polynomial continuously from the coefficients.
In constructivist constructive mathematics or intuitionistic logic, the story may be is different, as Francois Dorais explains in his answer.