What's your process of learning Coq? I have to confess that 'proof automation' is one of those shortcomings I never overcame. Even going through your well-documented code took me a shameful amount of time, and that's after you've done all the heavy lifting. Agreed on Idris, but, per your recommendation back from IRC dwelling days, I found Type-Driven Development with Idris by E. Brady as much more accessible. In this case, it means "I went farther into it than into any Coq tutorial". :P
It feels like most Coq documentation and tutorials are written for people getting Ivy-league graduate degrees where they can just pop over to any number of professors or fellow students to ask a quick question or get a decent idea of what the "right" way to do something is. Not having any of that, it's a bit tricky. I started very simple, proving basic logic statements and getting the hang of those tactics, then branched out a bit into proving things about numbers and lists. A fair bit of that came from Coq in a Hurry. From there, Coq'Art is a dated but good resource for the questions Coq in a Hurry doesn't answer. Most of the proofs mostly work, but some of the tactics are different now? However, even with those resources, I still find myself spending a lot of time looking around on the internet, finding bits and pieces in various disorganized places. Coq's standard library documentation is also horrendous and the various search commands in the language sometimes miss things for no apparent reason. And the error messages are only marginally useful. That said, once you get a feel for its eccentricities it is pretty fun, and learning it has helped me get better at writing proofs even in informal settings! Anyway, all this is to say maybe I should have learned Agda but I have to learn emacs first before I can make a fair call there :D