I’m having trouble finding elementary explanations of how to use Coq.

Let’s say I make a Coq file with some definitions and theorems, and I want to use these in another file. How would I do that (with Emacs/Proof General)?

I think I have to make a _CoqProject file and compile my files and then import them. But I don’t know how to do any of this, or how to organize the files. I’m new to Coq and Emacs. My background is in Mathematics.