That's fair. I actually find Coq rather painful to use. It gives me the distinct impression that it has been designed/implemented by somebody who has never wri

That's fair. I actually find Coq rather painful to use. It gives me the distinct impression that it has been designed/implemented by somebody who has never written human-computer interfaces before. When it comes to adapting humans to Mathematics, or adapting Mathematics to humans - I prefer the latter.