For the math that you mention, I would suggest looking at mathlib (https://github.com/leanprover-community/mathlib). I agree that the foundations of Coq are somewhat distanced from the foundations most mathematicians are trained in. Lean/mathlib might be a bit more familiar, not sure. That said, I don't see any obstacles to developing classical real analysis or linear algebra in Coq, once you've gotten used to writing proofs in it.
I'm curious, which field of math do you work in?
Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis...