Definitely! Otherwise it’s hard to keep track of how each “proof instructions” are manipulating the goals. Definitely give coqide or proofgeneral a try !

By the way, the first chapter is a very good introduction to what formal proving is about !

Last but not least, for all those that are interested in looking into coq, it was very helpful to start learning the basics of Ocaml first (especially variant types) ;)