In ZFC, you define reals as you sketch, and then specify rationals, integers etc as specific subsets, then you get inclusions, which mainstream mathematics uses

In ZFC, you define reals as you sketch, and then specify rationals, integers etc as specific subsets, then you get inclusions, which mainstream mathematics uses without worries. And yes, mainstream mathematics is non-constructive (as is Isabelle/HOL). (I don't want to have a contentious discussion about FOMs, or which prover is best, just trying to sketch the trade-offs, and historical background.)