Error 0 sorry 0 으로 조건부 증명함

수학 공리 ZFC가 한계가 있어서 그간 증명 못한거엿움
Nuclearity 도입하니까 lean4로 풀림 repo에 파일 올려둠