Fill axioms2
I would like to use Z.compare_is_valid
somehow to prove compare_is_valid. Or generalize it somehow. But I do not see a way.
Should I just uncomment proof?
Edited by Guillaume Claret
I would like to use Z.compare_is_valid
somehow to prove compare_is_valid. Or generalize it somehow. But I do not see a way.
Should I just uncomment proof?