Proof General is a generic Emacs interface for proof assistants
(also known as interactive theorem provers).

It is supplied ready to use for the proof assistants Coq,
EasyCrypt, qrhl, and PhoX.

See https://proofgeneral.github.io/ for installation instructions
and online documentation.  Or browse the accompanying info manual:
(info-display-manual "ProofGeneral")

Regarding the Coq proof assistant, you may be interested in the
company-coq extension of ProofGeneral (also available in MELPA).