```When a proof is finally accepted by Coq it just means it is correct: the absence of mistakes mistake correct for readable or maintainable.``` https://github.com/math-comp/mcb/blob/master/tex/chProofLanguage.tex#L1549
When a proof is finally accepted by Coq it just means it is correct: the absence of mistakes mistake correct for readable or maintainable.https://github.com/math-comp/mcb/blob/master/tex/chProofLanguage.tex#L1549