I agree with you about Coq, although there are some very smart folks working on it. My concern is that most of the improvements I've heard of are not about usability directly (i.e., how fun and readable it is to work with). I also don't quite now of precise low-hanging fruits that would improve it in this direction, but hopefully theorem provers will get friendlier and easier to use as time advances. Also the library of lemmas other people have proved and one can just plug in is steadily growing, so that should also reduce the pain of proving new stuff...