This PR eliminates the dependency on mathlib for operations that don’t necessitate it. Specifically, it addresses proof reconstruction for integers. Note that proof reconstruction for reals still relies on mathlib, but this is expected since users interested in real numbers would typically import mathlib anyway.
This PR eliminates the dependency on mathlib for operations that don’t necessitate it. Specifically, it addresses proof reconstruction for integers. Note that proof reconstruction for reals still relies on mathlib, but this is expected since users interested in real numbers would typically import mathlib anyway.