What people are telling you is you need to check the signature of negative_one_has_a_real_square_root (which includes the definition of Real). Generally this is an easy task. Did you define things the way that you meant to define them to make the statement that you meant to make? Then you can trust that the 500k lines that prove it are fine.
If you just had what you have here in the middle of a 500k line proof of some other interesting statement whose definitions you properly validated, that would be okay. The names are weird for a human, but the mathematical content is correct.
If you just had what you have here in the middle of a 500k line proof of some other interesting statement whose definitions you properly validated, that would be okay. The names are weird for a human, but the mathematical content is correct.