Is there proof General for Coq in Atom

#1

Is there proof General for Coq in Atom?

#2

something I can use to actually check my code, not just highlight text

#3

Hmmm, not that I can see: