alt Hacker NewsSo add it as an axiom with a comment pointing to the proof. If you don't trust the proof because you don't personally understand it, why are you using a proof assistant in the first place?
So add it as an axiom with a comment pointing to the proof. If you don't trust the proof because you don't personally understand it, why are you using a proof assistant in the first place?