Don’t forget the source code of Coq itself. What you have written here is not a formal proof, it’s a series of instructions to Coq requesting it to generate the

Don’t forget the source code of Coq itself. What you have written here is not a formal proof, it’s a series of instructions to Coq requesting it to generate the proof for you. To know that you’ve proved it you need to inspect the output, otherwise you’re trusting the source code of Coq itself.